Documentation

Init.Notation

    Auxiliary type used to represent syntax categories. We mainly use auxiliary definitions with this type to attach doc strings to syntax categories.

    Instances For

      command is the syntax category for things that appear at the top level of a lean file. For example, def foo := 1 is a command, as is namespace Foo and end Foo. Commands generally have an effect on the state of adding something to the environment (like a new definition), as well as commands like variable which modify future commands within a scope.

      Equations
      Instances For

        term is the builtin syntax category for terms. A term denotes an expression in lean's type theory, for example 2 + 2 is a term. The difference between Term and Expr is that the former is a kind of syntax, while the latter is the result of elaboration. For example by simp is also a Term, but it elaborates to different Exprs depending on the context.

        Equations
        Instances For

          tactic is the builtin syntax category for tactics. These appear after by in proofs, and they are programs that take in the proof context (the hypotheses in scope plus the type of the term to synthesize) and construct a term of the expected type. For example, simp is a tactic, used in:

          example : 2 + 2 = 4 := by simp
          
          Equations
          Instances For

            doElem is a builtin syntax category for elements that can appear in the do notation. For example, let x ← e is a doElem, and a do block consists of a list of doElems.

            Equations
            Instances For

              level is a builtin syntax category for universe levels. This is the u in Sort u: it can contain max and imax, addition with constants, and variables.

              Equations
              Instances For

                attr is a builtin syntax category for attributes. Declarations can be annotated with attributes using the @[...] notation.

                Equations
                Instances For

                  stx is a builtin syntax category for syntax. This is the abbreviated parser notation used inside syntax and macro declarations.

                  Equations
                  Instances For

                    prio is a builtin syntax category for priorities. Priorities are used in many different attributes. Higher numbers denote higher priority, and for example typeclass search will try high priority instances before low priority. In addition to literals like 37, you can also use low, mid, high, as well as add and subtract priorities.

                    Equations
                    Instances For

                      prec is a builtin syntax category for precedences. A precedence is a value that expresses how tightly a piece of syntax binds: for example 1 + 2 * 3 is parsed as 1 + (2 * 3) because * has a higher pr0ecedence than +. Higher numbers denote higher precedence. In addition to literals like 37, there are some special named priorities:

                      • arg for the precedence of function arguments
                      • max for the highest precedence used in term parsers (not actually the maximum possible value)
                      • lead for the precedence of terms not supposed to be used as arguments and you can also add and subtract precedences.
                      Equations
                      Instances For

                        DSL for specifying parser precedences and priorities

                        Addition of precedences. This is normally used only for offseting, e.g. max + 1.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          Subtraction of precedences. This is normally used only for offseting, e.g. max - 1.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            Addition of priorities. This is normally used only for offseting, e.g. default + 1.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              Subtraction of priorities. This is normally used only for offseting, e.g. default - 1.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                • Lean.instCoeOutTSyntaxSyntax = { coe := fun stx => stx.raw }

                                Maximum precedence used in term parsers, in particular for terms in function position (ident, paren, ...)

                                Equations
                                Instances For

                                  Precedence used for application arguments (do, by, ...).

                                  Equations
                                  Instances For

                                    Precedence used for terms not supposed to be used as arguments (let, have, ...).

                                    Equations
                                    Instances For

                                      Parentheses are used for grouping precedence expressions.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        Minimum precedence used in term parsers.

                                        Equations
                                        Instances For

                                          (min+1) (we can only write min+1 after Meta.lean)

                                          Equations
                                          Instances For

                                            max:prec as a term. It is equivalent to eval_prec max for eval_prec defined at Meta.lean. We use max_prec to workaround bootstrapping issues.

                                            Equations
                                            Instances For

                                              The default priority default = 1000, which is used when no priority is set.

                                              Equations
                                              Instances For

                                                The standardized "low" priority low = 100, for things that should be lower than default priority.

                                                Equations
                                                Instances For

                                                  The standardized "medium" priority mid = 500. This is lower than default, and higher than low.

                                                  Equations
                                                  Instances For

                                                    The standardized "high" priority high = 10000, for things that should be higher than default priority.

                                                    Equations
                                                    Instances For

                                                      Parentheses are used for grouping priority expressions.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For

                                                        p+ is shorthand for many1(p). It uses parser p 1 or more times, and produces a nullNode containing the array of parsed results. This parser has arity 1.

                                                        If p has arity more than 1, it is auto-grouped in the items generated by the parser.

                                                        Equations
                                                        Instances For

                                                          p* is shorthand for many(p). It uses parser p 0 or more times, and produces a nullNode containing the array of parsed results. This parser has arity 1.

                                                          If p has arity more than 1, it is auto-grouped in the items generated by the parser.

                                                          Equations
                                                          Instances For

                                                            (p)? is shorthand for optional(p). It uses parser p 0 or 1 times, and produces a nullNode containing the array of parsed results. This parser has arity 1.

                                                            p is allowed to have arity n > 1 (in which case the node will have either 0 or n children), but if it has arity 0 then the result will be ambiguous.

                                                            Because ? is an identifier character, ident? will not work as intended. You have to write either ident ? or (ident)? for it to parse as the ? combinator applied to the ident parser.

                                                            Equations
                                                            Instances For

                                                              p1 <|> p2 is shorthand for orelse(p1, p2), and parses either p1 or p2. It does not backtrack, meaning that if p1 consumes at least one token then p2 will not be tried. Therefore, the parsers should all differ in their first token. The atomic(p) parser combinator can be used to locally backtrack a parser. (For full backtracking, consider using extensible syntax classes instead.)

                                                              On success, if the inner parser does not generate exactly one node, it will be automatically wrapped in a group node, so the result will always be arity 1.

                                                              The <|> combinator does not generate a node of its own, and in particular does not tag the inner parsers to distinguish them, which can present a problem when reconstructing the parse. A well formed <|> parser should use disjoint node kinds for p1 and p2.

                                                              Equations
                                                              Instances For

                                                                p,* is shorthand for sepBy(p, ","). It parses 0 or more occurrences of p separated by ,, that is: empty | p | p,p | p,p,p | ....

                                                                It produces a nullNode containing a SepArray with the interleaved parser results. It has arity 1, and auto-groups its component parser if needed.

                                                                Equations
                                                                Instances For

                                                                  p,+ is shorthand for sepBy(p, ","). It parses 1 or more occurrences of p separated by ,, that is: p | p,p | p,p,p | ....

                                                                  It produces a nullNode containing a SepArray with the interleaved parser results. It has arity 1, and auto-groups its component parser if needed.

                                                                  Equations
                                                                  Instances For

                                                                    p,*,? is shorthand for sepBy(p, ",", allowTrailingSep). It parses 0 or more occurrences of p separated by ,, possibly including a trailing ,, that is: empty | p | p, | p,p | p,p, | p,p,p | ....

                                                                    It produces a nullNode containing a SepArray with the interleaved parser results. It has arity 1, and auto-groups its component parser if needed.

                                                                    Equations
                                                                    Instances For

                                                                      p,+,? is shorthand for sepBy1(p, ",", allowTrailingSep). It parses 1 or more occurrences of p separated by ,, possibly including a trailing ,, that is: p | p, | p,p | p,p, | p,p,p | ....

                                                                      It produces a nullNode containing a SepArray with the interleaved parser results. It has arity 1, and auto-groups its component parser if needed.

                                                                      Equations
                                                                      Instances For

                                                                        !p parses the negation of p. That is, it fails if p succeeds, and otherwise parses nothing. It has arity 0.

                                                                        Equations
                                                                        Instances For

                                                                          The nat_lit n macro constructs "raw numeric literals". This corresponds to the Expr.lit (.natVal n) constructor in the Expr data type.

                                                                          Normally, when you write a numeral like #check 37, the parser turns this into an application of OfNat.ofNat to the raw literal 37 to cast it into the target type, even if this type is Nat (so the cast is the identity function). But sometimes it is necessary to talk about the raw numeral directly, especially when proving properties about the ofNat function itself.

                                                                          Equations
                                                                          Instances For

                                                                            Function composition is the act of pipelining the result of one function, to the input of another, creating an entirely new function. Example:

                                                                            #eval Function.comp List.reverse (List.drop 2) [3, 2, 4, 1]
                                                                            -- [1, 4]
                                                                            

                                                                            You can use the notation f ∘ g as shorthand for Function.comp f g.

                                                                            #eval (List.reverse ∘ List.drop 2) [3, 2, 4, 1]
                                                                            -- [1, 4]
                                                                            

                                                                            A simpler way of thinking about it, is that List.reverseList.drop 2 is equivalent to fun xs => List.reverse (List.drop 2 xs), the benefit is that the meaning of composition is obvious, and the representation is compact.

                                                                            Equations
                                                                            Instances For

                                                                              Product type (aka pair). You can use α × β as notation for Prod α β. Given a : α and b : β, Prod.mk a b : Prod α β. You can use (a, b) as notation for Prod.mk a b. Moreover, (a, b, c) is notation for Prod.mk a (Prod.mk b c). Given p : Prod α β, p.1 : α and p.2 : β. They are short for Prod.fst p and Prod.snd p respectively. You can also write p.fst and p.snd. For more information: Constructors with Arguments

                                                                              Equations
                                                                              Instances For

                                                                                a ||| b computes the bitwise OR of a and b. The meaning of this notation is type-dependent.

                                                                                Equations
                                                                                Instances For

                                                                                  a ^^^ b computes the bitwise XOR of a and b. The meaning of this notation is type-dependent.

                                                                                  Equations
                                                                                  Instances For

                                                                                    a &&& b computes the bitwise AND of a and b. The meaning of this notation is type-dependent.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For

                                                                                      a + b computes the sum of a and b. The meaning of this notation is type-dependent.

                                                                                      Equations
                                                                                      Instances For

                                                                                        a - b computes the difference of a and b. The meaning of this notation is type-dependent.

                                                                                        • For natural numbers, this operator saturates at 0: a - b = 0 when a ≤ b.
                                                                                        Equations
                                                                                        Instances For

                                                                                          a * b computes the product of a and b. The meaning of this notation is type-dependent.

                                                                                          Equations
                                                                                          Instances For

                                                                                            a / b computes the result of dividing a by b. The meaning of this notation is type-dependent.

                                                                                            • For most types like Nat, Int, Rat, Real, a / 0 is defined to be 0.
                                                                                            • For Nat and Int, a / b rounds toward 0.
                                                                                            • For Float, a / 0 follows the IEEE 754 semantics for division, usually resulting in inf or nan.
                                                                                            Equations
                                                                                            Instances For

                                                                                              a % b computes the remainder upon dividing a by b. The meaning of this notation is type-dependent.

                                                                                              • For Nat and Int, a % 0 is defined to be a.
                                                                                              Equations
                                                                                              Instances For

                                                                                                a <<< b computes a shifted to the left by b places. The meaning of this notation is type-dependent.

                                                                                                • On Nat, this is equivalent to a * 2 ^ b.
                                                                                                • On UInt8 and other fixed width unsigned types, this is the same but truncated to the bit width.
                                                                                                Equations
                                                                                                Instances For

                                                                                                  a >>> b computes a shifted to the right by b places. The meaning of this notation is type-dependent.

                                                                                                  • On Nat and fixed width unsigned types like UInt8, this is equivalent to a / 2 ^ b.
                                                                                                  Equations
                                                                                                  Instances For

                                                                                                    a ^ b computes a to the power of b. The meaning of this notation is type-dependent.

                                                                                                    Equations
                                                                                                    Instances For

                                                                                                      a ++ b is the result of concatenation of a and b, usually read "append". The meaning of this notation is type-dependent.

                                                                                                      Equations
                                                                                                      Instances For

                                                                                                        -a computes the negative or opposite of a. The meaning of this notation is type-dependent.

                                                                                                        Equations
                                                                                                        Instances For

                                                                                                          The implementation of ~~~a : α.

                                                                                                          Equations
                                                                                                          Instances For

                                                                                                            Remark: the infix commands above ensure a delaborator is generated for each relations. We redefine the macros below to be able to use the auxiliary binop% elaboration helper for binary operators. It addresses issue #382.

                                                                                                            The less-equal relation: x ≤ y

                                                                                                            Equations
                                                                                                            Instances For

                                                                                                              The less-equal relation: x ≤ y

                                                                                                              Equations
                                                                                                              Instances For

                                                                                                                The less-than relation: x < y

                                                                                                                Equations
                                                                                                                Instances For

                                                                                                                  a ≥ b is an abbreviation for b ≤ a.

                                                                                                                  Equations
                                                                                                                  Instances For

                                                                                                                    a ≥ b is an abbreviation for b ≤ a.

                                                                                                                    Equations
                                                                                                                    Instances For

                                                                                                                      a > b is an abbreviation for b < a.

                                                                                                                      Equations
                                                                                                                      Instances For

                                                                                                                        The equality relation. It has one introduction rule, Eq.refl. We use a = b as notation for Eq a b. A fundamental property of equality is that it is an equivalence relation.

                                                                                                                        variable (α : Type) (a b c d : α)
                                                                                                                        variable (hab : a = b) (hcb : c = b) (hcd : c = d)
                                                                                                                        
                                                                                                                        example : a = d :=
                                                                                                                          Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
                                                                                                                        

                                                                                                                        Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given h1 : a = b and h2 : p a, we can construct a proof for p b using substitution: Eq.subst h1 h2. Example:

                                                                                                                        example (α : Type) (a b : α) (p : α → Prop)
                                                                                                                                (h1 : a = b) (h2 : p a) : p b :=
                                                                                                                          Eq.subst h1 h2
                                                                                                                        
                                                                                                                        example (α : Type) (a b : α) (p : α → Prop)
                                                                                                                            (h1 : a = b) (h2 : p a) : p b :=
                                                                                                                          h1 ▸ h2
                                                                                                                        

                                                                                                                        The triangle in the second presentation is a macro built on top of Eq.subst and Eq.symm, and you can enter it by typing \t. For more information: Equality

                                                                                                                        Equations
                                                                                                                        Instances For

                                                                                                                          Boolean equality, notated as a == b.

                                                                                                                          Equations
                                                                                                                          Instances For

                                                                                                                            Remark: the infix commands above ensure a delaborator is generated for each relations. We redefine the macros below to be able to use the auxiliary binrel% elaboration helper for binary relations. It has better support for applying coercions. For example, suppose we have binrel% Eq n i where n : Nat and i : Int. The default elaborator fails because we don't have a coercion from Int to Nat, but binrel% succeeds because it also tries a coercion from Nat to Int even when the nat occurs before the int.

                                                                                                                            And a b, or a ∧ b, is the conjunction of propositions. It can be constructed and destructed like a pair: if ha : a and hb : b then ⟨ha, hb⟩ : a ∧ b, and if h : a ∧ b then h.left : a and h.right : b.

                                                                                                                            Equations
                                                                                                                            Instances For

                                                                                                                              And a b, or a ∧ b, is the conjunction of propositions. It can be constructed and destructed like a pair: if ha : a and hb : b then ⟨ha, hb⟩ : a ∧ b, and if h : a ∧ b then h.left : a and h.right : b.

                                                                                                                              Equations
                                                                                                                              Instances For

                                                                                                                                Or a b, or a ∨ b, is the disjunction of propositions. There are two constructors for Or, called Or.inl : a → a ∨ b and Or.inr : b → a ∨ b, and you can use match or cases to destruct an Or assumption into the two cases.

                                                                                                                                Equations
                                                                                                                                Instances For

                                                                                                                                  Or a b, or a ∨ b, is the disjunction of propositions. There are two constructors for Or, called Or.inl : a → a ∨ b and Or.inr : b → a ∨ b, and you can use match or cases to destruct an Or assumption into the two cases.

                                                                                                                                  Equations
                                                                                                                                  Instances For

                                                                                                                                    Not p, or ¬p, is the negation of p. It is defined to be p → False, so if your goal is ¬p you can use intro h to turn the goal into h : p ⊢ False, and if you have hn : ¬p and h : p then hn h : False and (hn h).elim will prove anything. For more information: Propositional Logic

                                                                                                                                    Equations
                                                                                                                                    Instances For

                                                                                                                                      and x y, or x && y, is the boolean "and" operation (not to be confused with And : Prop → Prop → Prop, which is the propositional connective). It is @[macro_inline] because it has C-like short-circuiting behavior: if x is false then y is not evaluated.

                                                                                                                                      Equations
                                                                                                                                      Instances For

                                                                                                                                        or x y, or x || y, is the boolean "or" operation (not to be confused with Or : Prop → Prop → Prop, which is the propositional connective). It is @[macro_inline] because it has C-like short-circuiting behavior: if x is true then y is not evaluated.

                                                                                                                                        Equations
                                                                                                                                        Instances For

                                                                                                                                          not x, or !x, is the boolean "not" operation (not to be confused with Not : Prop → Prop, which is the propositional connective).

                                                                                                                                          Equations
                                                                                                                                          Instances For

                                                                                                                                            The membership relation a ∈ s : Prop where a : α, s : γ.

                                                                                                                                            Equations
                                                                                                                                            Instances For

                                                                                                                                              a ∉ b is negated elementhood. It is notation for ¬ (a ∈ b).

                                                                                                                                              Equations
                                                                                                                                              Instances For

                                                                                                                                                If a : α and l : List α, then cons a l, or a :: l, is the list whose first element is a and with l as the rest of the list.

                                                                                                                                                Equations
                                                                                                                                                Instances For

                                                                                                                                                  a <|> b executes a and returns the result, unless it fails in which case it executes and returns b. Because b is not always executed, it is passed as a thunk so it can be forced only when needed. The meaning of this notation is type-dependent.

                                                                                                                                                  Equations
                                                                                                                                                  Instances For

                                                                                                                                                    a >> b executes a, ignores the result, and then executes b. If a fails then b is not executed. Because b is not always executed, it is passed as a thunk so it can be forced only when needed. The meaning of this notation is type-dependent.

                                                                                                                                                    Equations
                                                                                                                                                    Instances For

                                                                                                                                                      If x : m α and f : α → m β, then x >>= f : m β represents the result of executing x to get a value of type α and then passing it to f.

                                                                                                                                                      Equations
                                                                                                                                                      Instances For

                                                                                                                                                        If mf : F (α → β) and mx : F α, then mf <*> mx : F β. In a monad this is the same as do let f ← mf; x ← mx; pure (f x): it evaluates first the function, then the argument, and applies one to the other.

                                                                                                                                                        To avoid surprising evaluation semantics, mx is taken "lazily", using a Unit → f α function.

                                                                                                                                                        Equations
                                                                                                                                                        Instances For

                                                                                                                                                          If x : F α and y : F β, then x <* y evaluates x, then y, and returns the result of x.

                                                                                                                                                          To avoid surprising evaluation semantics, y is taken "lazily", using a Unit → f β function.

                                                                                                                                                          Equations
                                                                                                                                                          Instances For

                                                                                                                                                            If x : F α and y : F β, then x *> y evaluates x, then y, and returns the result of y.

                                                                                                                                                            To avoid surprising evaluation semantics, y is taken "lazily", using a Unit → f β function.

                                                                                                                                                            Equations
                                                                                                                                                            Instances For

                                                                                                                                                              If f : α → β and x : F α then f <$> x : F β.

                                                                                                                                                              Equations
                                                                                                                                                              Instances For

                                                                                                                                                                binderIdent matches an ident or a _. It is used for identifiers in binding position, where _ means that the value should be left unnamed and inaccessible.

                                                                                                                                                                Equations
                                                                                                                                                                Instances For

                                                                                                                                                                  A case tag argument has the form tag x₁ ... xₙ; it refers to tag tag and renames the last n hypotheses to x₁ ... xₙ.

                                                                                                                                                                  Equations
                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                  Instances For

                                                                                                                                                                    "Dependent" if-then-else, normally written via the notation if h : c then t(h) else e(h), is sugar for dite c (fun h => t(h)) (fun h => e(h)), and it is the same as if c then t else e except that t is allowed to depend on a proof h : c, and e can depend on h : ¬c. (Both branches use the same name for the hypothesis, even though it has different types in the two cases.)

                                                                                                                                                                    We use this to be able to communicate the if-then-else condition to the branches. For example, Array.get arr ⟨i, h⟩ expects a proof h : i < arr.size in order to avoid a bounds check, so you can write if h : i < arr.size then arr.get ⟨i, h⟩ else ... to avoid the bounds check inside the if branch. (Of course in this case we have only lifted the check into an explicit if, but we could also use this proof multiple times or derive i < arr.size from some other proposition that we are checking in the if.)

                                                                                                                                                                    Equations
                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                    Instances For

                                                                                                                                                                      if c then t else e is notation for ite c t e, "if-then-else", which decides to return t or e depending on whether c is true or false. The explicit argument c : Prop does not have any actual computational content, but there is an additional [Decidable c] argument synthesized by typeclass inference which actually determines how to evaluate c to true or false.

                                                                                                                                                                      Because lean uses a strict (call-by-value) evaluation strategy, the signature of this function is problematic in that it would require t and e to be evaluated before calling the ite function, which would cause both sides of the if to be evaluated. Even if the result is discarded, this would be a big performance problem, and is undesirable for users in any case. To resolve this, ite is marked as @[macro_inline], which means that it is unfolded during code generation, and the definition of the function uses fun _ => t and fun _ => e so this recovers the expected "lazy" behavior of if: the t and e arguments delay evaluation until c is known.

                                                                                                                                                                      Equations
                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                      Instances For

                                                                                                                                                                        if let pat := d then t else e is a shorthand syntax for:

                                                                                                                                                                        match d with
                                                                                                                                                                        | pat => t
                                                                                                                                                                        | _ => e
                                                                                                                                                                        

                                                                                                                                                                        It matches d against the pattern pat and the bindings are available in t. If the pattern does not match, it returns e instead.

                                                                                                                                                                        Equations
                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                        Instances For

                                                                                                                                                                          cond b x y is the same as if b then x else y, but optimized for a boolean condition. It can also be written as bif b then x else y. This is @[macro_inline] because x and y should not be eagerly evaluated (see ite).

                                                                                                                                                                          Equations
                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                          Instances For

                                                                                                                                                                            Haskell-like pipe operator <|. f <| x means the same as the same as f x, except that it parses x with lower precedence, which means that f <| g <| x is interpreted as f (g x) rather than (f g) x.

                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For

                                                                                                                                                                              Haskell-like pipe operator |>. x |> f means the same as the same as f x, and it chains such that x |> f |> g is interpreted as g (f x).

                                                                                                                                                                              Equations
                                                                                                                                                                              Instances For

                                                                                                                                                                                Alternative syntax for <|. f $ x means the same as the same as f x, except that it parses x with lower precedence, which means that f $ g $ x is interpreted as f (g x) rather than (f g) x.

                                                                                                                                                                                Equations
                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                Instances For

                                                                                                                                                                                  Subtype p, usually written as {x : α // p x}, is a type which represents all the elements x : α for which p x is true. It is structurally a pair-like type, so if you have x : α and h : p x then ⟨x, h⟩ : {x // p x}. An element s : {x // p x} will coerce to α but you can also make it explicit using s.1 or s.val.

                                                                                                                                                                                  Equations
                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                  Instances For

                                                                                                                                                                                    without_expected_type t instructs Lean to elaborate t without an expected type. Recall that terms such as match ... with ... and ⟨...⟩ will postpone elaboration until expected type is known. So, without_expected_type is not effective in this case.

                                                                                                                                                                                    Equations
                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                    Instances For

                                                                                                                                                                                      The syntax [a, b, c] is shorthand for a :: b :: c :: [], or List.cons a (List.cons b (List.cons c List.nil)). It allows conveniently constructing list literals.

                                                                                                                                                                                      For lists of length at least 64, an alternative desugaring strategy is used which uses let bindings as intermediates as in let left := [d, e, f]; a :: b :: c :: left to avoid creating very deep expressions. Note that this changes the order of evaluation, although it should not be observable unless you use side effecting operations like dbg_trace.

                                                                                                                                                                                      Equations
                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                      Instances For

                                                                                                                                                                                        Auxiliary syntax for implementing [$elem,*] list literal syntax. The syntax %[a,b,c|tail] constructs a value equivalent to a::b::c::tail. It uses binary partitioning to construct a tree of intermediate let bindings as in let left := [d, e, f]; a :: b :: c :: left to avoid creating very deep expressions.

                                                                                                                                                                                        Equations
                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                        Instances For

                                                                                                                                                                                          Category for carrying raw syntax trees between macros; any content is printed as is by the pretty printer. The only accepted parser for this category is an antiquotation.

                                                                                                                                                                                          Equations
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            Equations
                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                            Instances For

                                                                                                                                                                                              with_annotate_term stx e annotates the lexical range of stx : Syntax with term info for e.

                                                                                                                                                                                              Equations
                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                              Instances For

                                                                                                                                                                                                The attribute @[deprecated] on a declaration indicates that the declaration is discouraged for use in new code, and/or should be migrated away from in existing code. It may be removed in a future version of the library.

                                                                                                                                                                                                @[deprecated myBetterDef] means that myBetterDef is the suggested replacement.

                                                                                                                                                                                                Equations
                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                Instances For

                                                                                                                                                                                                  When parent_dir contains the current Lean file, include_str "path" / "to" / "file" becomes a string literal with the contents of the file at "parent_dir" / "path" / "to" / "file". If this file cannot be read, elaboration fails.

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  Instances For