Documentation

Lean.Parser.Term

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

    A docComment parses a "documentation comment" like /-- foo -/. This is not treated like a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.

    A docComment node contains a /-- atom and then the remainder of the comment, foo -/ in this example. Use TSyntax.getDocString to extract the body text from a doc string syntax node.

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

      sepByIndentSemicolon(p) parses a sequence of p optionally followed by ;, similar to manyIndent(p ";"?), except that if two occurrences of p occur on the same line, the ; is mandatory. This is used by tactic parsing, so that

      example := by
        skip
        skip
      

      is legal, but by skip skip is not - it must be written as by skip; skip.

      Equations
      Instances For

        sepBy1IndentSemicolon(p) parses a (nonempty) sequence of p optionally followed by ;, similar to many1Indent(p ";"?), except that if two occurrences of p occur on the same line, the ; is mandatory. This is used by tactic parsing, so that

        example := by
          skip
          skip
        

        is legal, but by skip skip is not - it must be written as by skip; skip.

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

            The syntax { tacs } is an alternative syntax for · tacs. It runs the tactics in sequence, and fails if the goal is not solved.

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

              A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics. Delimiter-free indentation is determined by the first tactic of the sequence.

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

                Same as [tacticSeq] but requires delimiter-free tactic sequence to have strict indentation. The strict indentation requirement only apply to nested bys, as top-level bys do not have a position set.

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

                    Built-in parsers #

                    by tac constructs a term of the expected type by running the tactic(s) tac.

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

                        A type universe. Type ≡ Type 0, Type u ≡ Sort (u + 1).

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

                          A specific universe in Lean's infinite hierarchy of universes.

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

                            The universe of propositions. Prop ≡ Sort 0.

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

                              A placeholder term, to be synthesized by unification.

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

                                Parses a "synthetic hole", that is, ?foo or ?_. This syntax is used to construct named metavariables.

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

                                  The term denotes a term that was omitted by the pretty printer. The presence of in pretty printer output is controlled by the pp.deepTerms and pp.proofs options, and these options can be further adjusted using pp.deepTerms.threshold and pp.proofs.threshold.

                                  It is only meant to be used for pretty printing. However, in case it is copied and pasted from the Infoview, logs a warning and elaborates like _.

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

                                    A temporary placeholder for a missing proof or value.

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

                                      A placeholder for an implicit lambda abstraction's variable. The lambda abstraction is scoped to the surrounding parentheses. For example, (· + ·) is equivalent to fun x y => x + y.

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

                                        Type ascription notation: (0 : Int) instructs Lean to process 0 as a value of type Int. An empty type ascription (e :) elaborates e without the expected type. This is occasionally useful when Lean's heuristics for filling arguments from the expected type do not yield the right result.

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

                                          Tuple notation; () is short for Unit.unit, (a, b, c) for Prod.mk a (Prod.mk b c), etc.

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

                                            Parentheses, used for grouping expressions (e.g., a * (b + c)). Can also be used for creating simple functions when combined with ·. Here are some examples:

                                            • (· + 1) is shorthand for fun x => x + 1
                                            • (· + ·) is shorthand for fun x y => x + y
                                            • (f · a b) is shorthand for fun x => f x a b
                                            • (h (· + 1) ·) is shorthand for fun x => h (fun y => y + 1) x
                                            • also applies to other parentheses-like notations such as (·, 1)
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For

                                              The anonymous constructor ⟨e, ...⟩ is equivalent to c e ... if the expected type is an inductive type with a single constructor c. If more terms are given than c has parameters, the remaining arguments are turned into a new anonymous constructor application. For example, ⟨a, b, c⟩ : α × (β × γ) is equivalent to ⟨a, ⟨b, c⟩⟩.

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

                                                  A sufficesDecl represents everything that comes after the suffices keyword: an optional x :, then a term ty, then from val or by tac.

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

                                                                  Structure instance. { x := e, ... } assigns e to field x, which may be inherited. If e is itself a variable called x, it can be elided: fun y => { x := 1, y }. A structure update of an existing value can be given via with: { point with x := 1 }. The structure type can be specified if not inferable: { x := 1, y := 2 : Point }.

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

                                                                      @x disables automatic insertion of implicit parameters of the constant x. @e for any term e also disables the insertion of implicit lambdas at this position.

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

                                                                        .(e) marks an "inaccessible pattern", which does not influence evaluation of the pattern match, but may be necessary for type-checking. In contrast to regular patterns, e may be an arbitrary term of the appropriate type.

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

                                                                                  Explicit binder, like (x y : A) or (x y). Default values can be specified using (x : A := v) syntax, and tactics using (x : A := by tac).

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

                                                                                    Implicit binder, like {x y : A} or {x y}. In regular applications, whenever all parameters before it have been specified, then a _ placeholder is automatically inserted for this parameter. Implicit parameters should be able to be determined from the other arguments and the return type by unification.

                                                                                    In @ explicit mode, implicit binders behave like explicit binders.

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

                                                                                          Strict-implicit binder, like ⦃x y : A⦄ or ⦃x y⦄. In contrast to { ... } implicit binders, strict-implicit binders do not automatically insert a _ placeholder until at least one subsequent explicit parameter is specified. Do not use strict-implicit binders unless there is a subsequent explicit parameter. Assuming this rule is followed, for fully applied expressions implicit and strict-implicit binders have the same behavior.

                                                                                          Example: If h : ∀ ⦃x : A⦄, x ∈ s → p x and hs : y ∈ s, then h by itself elaborates to itself without inserting _ for the x : A parameter, and h hs has type p y. In contrast, if h' : ∀ {x : A}, x ∈ s → p x, then h by itself elaborates to have type ?m ∈ s → p ?m with ?m a fresh metavariable.

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

                                                                                            Instance-implicit binder, like [C] or [inst : C]. In regular applications without @ explicit mode, it is automatically inserted and solved for by typeclass inference for the specified class C. In @ explicit mode, if _ is used for an instance-implicit parameter, then it is still solved for by typeclass inference; use (_) to inhibit this and have it be solved for by unification instead, like an implicit argument.

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

                                                                                              A bracketedBinder matches any kind of binder group that uses some kind of brackets:

                                                                                              • An explicit binder like (x y : A)
                                                                                              • An implicit binder like {x y : A}
                                                                                              • A strict implicit binder, ⦃y z : A⦄ or its ASCII alternative {{y z : A}}
                                                                                              • An instance binder [A] or [x : A] (multiple variables are not allowed here)
                                                                                              Equations
                                                                                              • One or more equations did not get rendered due to their size.
                                                                                              Instances For
                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                Instances For
                                                                                                  Equations
                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                  Instances For
                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For

                                                                                                      Useful for syntax quotations. Note that generic patterns such as `(matchAltExpr| | ... => $rhs) should also work with other rhsParsers (of arity 1).

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        instance Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_lean :
                                                                                                        Coe (Lean.TSyntax `Lean.Parser.Term.matchAltExpr) (Lean.TSyntax `Lean.Parser.Term.matchAlt)
                                                                                                        Equations
                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For

                                                                                                          matchDiscr matches a "match discriminant", either h : tm or tm, used in match as match h1 : e1, e2, h3 : e3 with ....

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

                                                                                                                    Pattern matching. match e, ... with | p, ... => f | ... matches each given term e against each pattern p of a match alternative. When all patterns of an alternative match, the match term evaluates to the value of the corresponding right-hand side f with the pattern variables bound to the respective matched values. If used as match h : e, ... with | p, ... => f | ..., h : e = p is available within f.

                                                                                                                    When not constructing a proof, match does not automatically substitute variables matched on in dependent variables' types. Use match (generalizing := true) ... to enforce this.

                                                                                                                    Syntax quotations can also be used in a pattern match. This matches a Syntax value against quotations, pattern variables, or _.

                                                                                                                    Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly.

                                                                                                                    Syntax.atoms are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in

                                                                                                                    syntax "c" ("foo" <|> "bar") ...
                                                                                                                    

                                                                                                                    foo and bar are indistinguishable during matching, but in

                                                                                                                    syntax foo := "foo"
                                                                                                                    syntax "c" (foo <|> "bar") ...
                                                                                                                    

                                                                                                                    they are not.

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

                                                                                                                      Empty match/ex falso. nomatch e is of arbitrary type α : Sort u if Lean can show that an empty set of patterns is exhaustive given e's type, e.g. because it has no constructors.

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

                                                                                                                                          Indicates that an argument to a function marked @[extern] is borrowed.

                                                                                                                                          Being borrowed only affects the ABI and runtime behavior of the function when compiled or interpreted. From the perspective of Lean's type system, this annotation has no effect. It similarly has no effect on functions not marked @[extern].

                                                                                                                                          When a function argument is borrowed, the function does not consume the value. This means that the function will not decrement the value's reference count or deallocate it, and the caller is responsible for doing so.

                                                                                                                                          Please see https://lean-lang.org/lean4/doc/dev/ffi.html#borrowing for a complete description.

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

                                                                                                                                            A literal of type Name.

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

                                                                                                                                              A resolved name literal. Evaluates to the full name of the given constant if existent in the current context, or else fails.

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

                                                                                                                                                          letDecl matches the body of a let declaration let f x1 x2 := e, let pat := e (where pat is an arbitrary term) or let f | pat1 => e1 | pat2 => e2 ... (a pattern matching declaration), except for the let keyword itself. let rec declarations are not handled here.

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

                                                                                                                                                            let is used to declare a local definition. Example:

                                                                                                                                                            let x := 1
                                                                                                                                                            let y := x + 1
                                                                                                                                                            x + y
                                                                                                                                                            

                                                                                                                                                            Since functions are first class citizens in Lean, you can use let to declare local functions too.

                                                                                                                                                            let double := fun x => 2*x
                                                                                                                                                            double (double 3)
                                                                                                                                                            

                                                                                                                                                            For recursive definitions, you should use let rec. You can also perform pattern matching using let. For example, assume p has type Nat × Nat, then you can write

                                                                                                                                                            let (x, y) := p
                                                                                                                                                            x + y
                                                                                                                                                            
                                                                                                                                                            Equations
                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                            Instances For

                                                                                                                                                              let_fun x := v; b is syntax sugar for (fun x => b) v. It is very similar to let x := v; b, but they are not equivalent. In let_fun, the value v has been abstracted away and cannot be accessed in b.

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

                                                                                                                                                                let_delayed x := v; b is similar to let x := v; b, but b is elaborated before v.

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

                                                                                                                                                                  let-declaration that is only included in the elaborated term if variable is still there. It is often used when building macros.

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

                                                                                                                                                                            haveDecl matches the body of a have declaration: have := e, have f x1 x2 := e, have pat := e (where pat is an arbitrary term) or have f | pat1 => e1 | pat2 => e2 ... (a pattern matching declaration), except for the have keyword itself.

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

                                                                                                                                                                                haveI behaves like have, but inlines the value instead of producing a let_fun term.

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

                                                                                                                                                                                  letI behaves like let, but inlines the value instead of producing a let_fun term.

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

                                                                                                                                                                                        attrKind matches ("scoped" <|> "local")?, used before an attribute like @[local simp].

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

                                                                                                                                                                                              Specify a termination argument for recursive functions.

                                                                                                                                                                                              termination_by a - b
                                                                                                                                                                                              

                                                                                                                                                                                              indicates that termination of the currently defined recursive function follows because the difference between the arguments a and b decreases.

                                                                                                                                                                                              If the function takes further argument after the colon, you can name them as follows:

                                                                                                                                                                                              def example (a : Nat) : NatNatNat :=
                                                                                                                                                                                              termination_by b c => a - b
                                                                                                                                                                                              

                                                                                                                                                                                              By default, a termination_by clause will cause the function to be constructed using well-founded recursion. The syntax termination_by structural a (or termination_by structural _ c => c) indicates the function is expected to be structural recursive on the argument. In this case the body of the termination_by clause must be one of the function's parameters.

                                                                                                                                                                                              If omitted, a termination argument will be inferred. If written as termination_by?, the inferrred termination argument will be suggested.

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

                                                                                                                                                                                                Specify a termination argument for recursive functions.

                                                                                                                                                                                                termination_by a - b
                                                                                                                                                                                                

                                                                                                                                                                                                indicates that termination of the currently defined recursive function follows because the difference between the arguments a and b decreases.

                                                                                                                                                                                                If the function takes further argument after the colon, you can name them as follows:

                                                                                                                                                                                                def example (a : Nat) : NatNatNat :=
                                                                                                                                                                                                termination_by b c => a - b
                                                                                                                                                                                                

                                                                                                                                                                                                By default, a termination_by clause will cause the function to be constructed using well-founded recursion. The syntax termination_by structural a (or termination_by structural _ c => c) indicates the function is expected to be structural recursive on the argument. In this case the body of the termination_by clause must be one of the function's parameters.

                                                                                                                                                                                                If omitted, a termination argument will be inferred. If written as termination_by?, the inferrred termination argument will be suggested.

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

                                                                                                                                                                                                  Manually prove that the termination argument (as specified with termination_by or inferred) decreases at each recursive call.

                                                                                                                                                                                                  By default, the tactic decreasing_tactic is used.

                                                                                                                                                                                                  Forces the use of well-founded recursion and is hence incompatible with termination_by structural.

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

                                                                                                                                                                                                    Termination hints are termination_by and decreasing_by, in that order.

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

                                                                                                                                                                                                      letRecDecl matches the body of a let-rec declaration: a doc comment, attributes, and then a let declaration without the let keyword, such as /-- foo -/ @[simp] bar := 1.

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

                                                                                                                                                                                                        letRecDecls matches letRecDecl,+, a comma-separated list of let-rec declarations (see letRecDecl).

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

                                                                                                                                                                                                                  unsafe t : α is an expression constructor which allows using unsafe declarations inside the body of t : α, by creating an auxiliary definition containing t and using implementedBy to wrap it in a safe interface. It is required that α is nonempty for this to be sound, but even beyond that, an unsafe block should be carefully inspected for memory safety because the compiler is unable to guarantee the safety of the operation.

                                                                                                                                                                                                                  For example, the evalExpr function is unsafe, because the compiler cannot guarantee that when you call evalExpr Foo ``Foo e that the type Foo corresponds to the name Foo, but in a particular use case, we can ensure this, so unsafe (evalExpr Foo ``Foo e) is a correct usage.

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

                                                                                                                                                                                                                    binrel% r a b elaborates r a b as a binary relation using the type propagation protocol in Lean.Elab.Extra.

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

                                                                                                                                                                                                                      binrel_no_prop% r a b is similar to binrel% r a b, but it coerces Prop arguments into Bool.

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

                                                                                                                                                                                                                        binop% f a b elaborates f a b as a binary operation using the type propagation protocol in Lean.Elab.Extra.

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

                                                                                                                                                                                                                          binop_lazy% is similar to binop% f a b, but it wraps b as a function from Unit.

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

                                                                                                                                                                                                                            leftact% f a b elaborates f a b as a left action using the type propagation protocol in Lean.Elab.Extra. In particular, it is like a unary operation with a fixed parameter a, where only the right argument b participates in the operator coercion elaborator.

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

                                                                                                                                                                                                                              rightact% f a b elaborates f a b as a right action using the type propagation protocol in Lean.Elab.Extra. In particular, it is like a unary operation with a fixed parameter b, where only the left argument a participates in the operator coercion elaborator.

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

                                                                                                                                                                                                                                unop% f a elaborates f a as a unary operation using the type propagation protocol in Lean.Elab.Extra.

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

                                                                                                                                                                                                                                      A macro which evaluates to the name of the currently elaborating declaration.

                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                        • with_decl_name% id e elaborates e in a context while changing the effective declaration name to id.
                                                                                                                                                                                                                                        • with_decl_name% ?id e does the same, but resolves id as a new definition name (appending the current namespaces).
                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                  clear% x; e elaborates x after clearing the free variable x from the local context. If x cannot be cleared (due to dependencies), it will keep x without failing.

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

                                                                                                                                                                                                                                                              Helper parser for marking match-alternatives that should not trigger errors if unused. We use them to implement macro_rules and elab_rules

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

                                                                                                                                                                                                                                                                      The extended field notation e.f is roughly short for T.f e where T is the type of e. More precisely,

                                                                                                                                                                                                                                                                      • if e is of a function type, e.f is translated to Function.f (p := e) where p is the first explicit parameter of function type
                                                                                                                                                                                                                                                                      • if e is of a named type T ... and there is a declaration T.f (possibly from export), e.f is translated to T.f (p := e) where p is the first explicit parameter of type T ...
                                                                                                                                                                                                                                                                      • otherwise, if e is of a structure type, the above is repeated for every base type of the structure.

                                                                                                                                                                                                                                                                      The field index notation e.i, where i is a positive number, is short for accessing the i-th field (1-indexed) of e if it is of a structure type.

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

                                                                                                                                                                                                                                                                            Syntax kind for syntax nodes representing the field of a projection in the InfoTree. Specifically, the InfoTree node for a projection s.f contains a child InfoTree node with syntax (Syntax.node .none identProjKind #[`f]).

                                                                                                                                                                                                                                                                            This is necessary because projection syntax cannot always be detected purely syntactically (s.f may refer to either the identifier s.f or a projection s.f depending on the available context).

                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                x.{u, ...} explicitly specifies the universes u, ... of the constant x.

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

                                                                                                                                                                                                                                                                                  x@e or x@h:e matches the pattern e and binds its value to the identifier x. If present, the identifier h is bound to a proof of x = e.

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

                                                                                                                                                                                                                                                                                    e |>.x is a shorthand for (e).x. It is especially useful for avoiding parentheses with repeated applications.

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

                                                                                                                                                                                                                                                                                      h ▸ e is a macro built on top of Eq.rec and Eq.symm definitions. Given h : a = b and e : p a, the term h ▸ e has type p b. You can also view h ▸ e as a "type casting" operation where you change the type of e by using h.

                                                                                                                                                                                                                                                                                      The macro tries both orientations of h. If the context provides an expected type, it rewrites the expected type, else it rewrites the type of e`.

                                                                                                                                                                                                                                                                                      See the Chapter "Quantifiers and Equality" in the manual "Theorem Proving in Lean" for additional information.

                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                          instance Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_lean_1 :
                                                                                                                                                                                                                                                                                          Coe (Lean.TSyntax `Lean.Parser.Term.bracketedBinderF) (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)
                                                                                                                                                                                                                                                                                          Equations

                                                                                                                                                                                                                                                                                          panic! msg formally evaluates to @Inhabited.default α if the expected type α implements Inhabited. At runtime, msg and the file position are printed to stderr unless the C function lean_set_panic_messages(false) has been executed before. If the C function lean_set_exit_on_panic(true) has been executed before, the process is then aborted.

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

                                                                                                                                                                                                                                                                                            A shorthand for panic! "unreachable code has been reached".

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

                                                                                                                                                                                                                                                                                              dbg_trace e; body evaluates to body and prints e (which can be an interpolated string literal) to stderr. It should only be used for debugging.

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

                                                                                                                                                                                                                                                                                                assert! cond panics if cond evaluates to false.

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

                                                                                                                                                                                                                                                                                                          Implementation of the show_term term elaborator.

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

                                                                                                                                                                                                                                                                                                            match_expr support.

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