def Lean.Parser.Command.docCommentOpen (sym : String) : Parser

Parses the opening delimiter sym of a documentation comment (/-- ... -/ or /-! ... -/).

Lean's whitespace parser considers comments to be whitespace, but the text of a documentation comment may begin with a comment marker, so the delimiter's trailing whitespace is only the substring that satisfies Char.isWhitespace.

Equations

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

def Lean.Parser.Command.docCommentOpen.formatter (sym : String) : PrettyPrinter.Formatter

Equations

• Lean.Parser.Command.docCommentOpen.formatter sym = Lean.PrettyPrinter.Formatter.symbolNoAntiquot.formatter sym

def Lean.Parser.Command.docCommentOpen.parenthesizer (sym : String) : PrettyPrinter.Parenthesizer

Equations

• Lean.Parser.Command.docCommentOpen.parenthesizer sym = Lean.PrettyPrinter.Parenthesizer.symbolNoAntiquot.parenthesizer sym

def Lean.Parser.Command.docCommentCloseFn : ParserFn

Parses the closing delimiter of a documentation comment at the current position, which finishCommentBlock has already matched, together with the whitespace after it.

Equations

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

def Lean.Parser.Command.versoCommentBodyFn : ParserFn

Equations

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

def Lean.Parser.Command.versoCommentBody : Parser

Equations

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

def Lean.Parser.Command.versoCommentBody.parenthesizer : PrettyPrinter.Parenthesizer

Equations

• Lean.Parser.Command.versoCommentBody.parenthesizer = Lean.PrettyPrinter.Parenthesizer.visitToken

def Lean.Parser.Command.versoCommentBody.formatter : PrettyPrinter.Formatter

Equations

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

def Lean.Parser.Command.commentBodyFn : ParserFn

Parses the text of a documentation comment that is not read as Verso markup, then its closing delimiter. The text is one atom whose trailing whitespace is the spaces and newlines before the closing delimiter, and the closing delimiter is an atom of its own.

Equations

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

def Lean.Parser.Command.commentBody : Parser

Equations

• Lean.Parser.Command.commentBody = Lean.Parser.node `Lean.Parser.Command.commentBody { fn := Lean.Parser.Command.commentBodyFn }

def Lean.Parser.Command.commentBody.parenthesizer : PrettyPrinter.Parenthesizer

Equations

• Lean.Parser.Command.commentBody.parenthesizer = Lean.PrettyPrinter.Parenthesizer.visitToken

def Lean.Parser.Command.commentBody.formatter : PrettyPrinter.Formatter

Equations

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

def Lean.Parser.Command.docComment : Parser

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.

At parse time, docComment checks the value of the doc.verso option. If it is true, the contents are parsed as Verso markup. If not, the contents are treated as plain text or Markdown. Use plainDocComment to always treat the contents as plain text.

A plain text doc comment node contains a /-- atom and then a node holding the comment's text as an atom and its closing -/ atom. Use TSyntax.getDocString to extract the text from a doc string syntax node. A Verso comment node contains the /-- atom, the document's syntax tree, and a closing -/ atom.

Equations

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

def Lean.Parser.Command.plainDocComment : Parser

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.

At parse time, docComment checks the value of the doc.verso option. If it is true, the contents are parsed as Verso markup. If not, the contents are treated as plain text or Markdown. Use plainDocComment to always treat the contents as plain text.

A plain text doc comment node contains a /-- atom and then a node holding the comment's text as an atom and its closing -/ atom. Use TSyntax.getDocString to extract the text from a doc string syntax node. A Verso comment node contains the /-- atom, the document's syntax tree, and a closing -/ atom.

Equations

• Lean.Parser.Command.plainDocComment = Lean.Doc.Parser.withoutVersoSyntax Lean.Parser.Command.docComment

def Lean.Parser.darrow : Parser

Equations

• Lean.Parser.darrow = Lean.Parser.symbol " => "

def Lean.Parser.semicolonOrLinebreak : Parser

Equations

• Lean.Parser.semicolonOrLinebreak = (Lean.Parser.symbol ";" <|> Lean.Parser.checkLinebreakBefore >> Lean.Parser.pushNone)

Built-in parsers

def Lean.Parser.Term.byTactic : Parser

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.

def Lean.Parser.Term.byTactic' : Parser

This is the same as byTactic, but it uses a different syntax kind. This is used by show and suffices instead of byTactic because these syntaxes don't support arbitrary terms where byTactic is accepted. Mathport uses this to e.g. safely find-replace by exact $e by $e in any context without causing incorrect syntax when the full expression is show $T by exact $e.

Equations

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

def Lean.Parser.Term.optSemicolon (p : Parser) : Parser

Equations

• Lean.Parser.Term.optSemicolon p = Lean.Parser.ppDedent (Lean.Parser.semicolonOrLinebreak >> Lean.Parser.ppLine >> p)

def Lean.Parser.Term.ident : Parser

Equations

• Lean.Parser.Term.ident = Lean.Parser.checkPrec Lean.Parser.maxPrec >> Lean.Parser.ident

def Lean.Parser.Term.num : Parser

Equations

• Lean.Parser.Term.num = Lean.Parser.checkPrec Lean.Parser.maxPrec >> Lean.Parser.numLit

def Lean.Parser.Term.scientific : Parser

Equations

• Lean.Parser.Term.scientific = Lean.Parser.checkPrec Lean.Parser.maxPrec >> Lean.Parser.scientificLit

def Lean.Parser.Term.str : Parser

Equations

• Lean.Parser.Term.str = Lean.Parser.checkPrec Lean.Parser.maxPrec >> Lean.Parser.strLit

def Lean.Parser.Term.char : Parser

Equations

• Lean.Parser.Term.char = Lean.Parser.checkPrec Lean.Parser.maxPrec >> Lean.Parser.charLit

def Lean.Parser.Term.type : Parser

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

Equations

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

def Lean.Parser.Term.sort : Parser

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

Equations

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

def Lean.Parser.Term.prop : Parser

The universe of propositions. Prop ≡ Sort 0.

Every proposition is propositionally equal to either True or False.

Equations

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

def Lean.Parser.Term.sorry : Parser

The sorry term is a temporary placeholder for a missing proof or value.

The syntax is intended for stubbing-out incomplete parts of a value or proof while still having a syntactically correct skeleton. Lean will give a warning whenever a declaration uses sorry, so you aren't likely to miss it, but you can double check if a declaration depends on sorry by looking for sorryAx in the output of the #print axioms my_thm command, the axiom used by the implementation of sorry.

"Go to definition" on sorry in the Infoview will go to the source position where it was introduced, if such information is available.

Each sorry is guaranteed to be unique, so for example the following fails:

example : (sorry : Nat) = sorry := rfl -- fails

See also the sorry tactic, which is short for exact sorry.

Equations

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

def Lean.Parser.Term.hygienicLParen : Parser

Equations

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

def Lean.Parser.Term.cdot : Parser

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. Tuple notation and type ascription notation also serve as scopes. Note that (· : ty) expands to ((fun x => x) : ty), so ty should be a function type.

Equations

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

def Lean.Parser.Term.typeAscription : Parser

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.

def Lean.Parser.Term.tuple : Parser

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

Conventions for notations in identifiers:

• The recommended spelling of (a, b) in identifiers is mk.

Equations

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

def Lean.Parser.Term.paren : Parser

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) and (· : Nat → Nat)

Equations

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

partial def Lean.Parser.Term.dropParens : Syntax → Syntax

Strip leading paren wrappers from stx.

def Lean.Parser.Term.anonymousCtor : Parser

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.

def Lean.Parser.Term.fromTerm : Parser

Equations

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

def Lean.Parser.Term.showRhs : Parser

Equations

• Lean.Parser.Term.showRhs = (Lean.Parser.Term.fromTerm <|> Lean.Parser.Term.byTactic')

def Lean.Parser.Term.sufficesDecl : Parser

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.

def Lean.Parser.Term.suffices : Parser

Equations

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

def Lean.Parser.Term.show : Parser

Equations

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

def Lean.Parser.Term.explicit : Parser

@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.

def Lean.Parser.Term.inaccessible : Parser

.(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.

def Lean.Parser.Term.depArrow : Parser

Equations

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

def Lean.Parser.Term.forall : Parser

Equations

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

def Lean.Parser.Term.matchAlt (rhsParser : Parser := termParser) : Parser

Equations

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

def Lean.Parser.Term.matchAltExpr : Parser

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

Equations

• Lean.Parser.Term.matchAltExpr = Lean.Parser.Term.matchAlt

@[instance_reducible]

instance Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_lean : Coe (TSyntax `Lean.Parser.Term.matchAltExpr) (TSyntax `Lean.Parser.Term.matchAlt)

Equations

• Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_lean = { coe := fun (stx : Lean.TSyntax `Lean.Parser.Term.matchAltExpr) => { raw := stx.raw } }

def Lean.Parser.Term.matchAlts (rhsParser : Parser := termParser) : Parser

Equations

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

def Lean.Parser.Term.matchDiscr : Parser

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.

def Lean.Parser.Term.trueVal : Parser

Equations

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

def Lean.Parser.Term.falseVal : Parser

Equations

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

def Lean.Parser.Term.generalizingParam : Parser

Equations

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

def Lean.Parser.Term.motive : Parser

Equations

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

def Lean.Parser.Term.match : Parser

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.

def Lean.Parser.Term.nomatch : Parser

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.

def Lean.Parser.Term.nofun : Parser

Equations

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

def Lean.Parser.Term.structInst : Parser

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.

def Lean.Parser.Term.structInstFieldDef : Parser

Equations

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

def Lean.Parser.Term.structInstFieldEqns : Parser

Equations

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

def Lean.Parser.Term.structInstDefault : Parser

Synthesizes a default value for a structure, making use of Inhabited instances for missing fields, as well as Inhabited instances for parent structures.

Equations

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

def Lean.Parser.Term.funImplicitBinder : Parser

Equations

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

def Lean.Parser.Term.funStrictImplicitBinder : Parser

Equations

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

def Lean.Parser.Term.funBinder : Parser

Equations

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

def Lean.Parser.Term.basicFun : Parser

Equations

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

def Lean.Parser.Term.fun : Parser

Equations

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

def Lean.Parser.Term.optExprPrecedence : Parser

Equations

• Lean.Parser.Term.optExprPrecedence = Lean.Parser.optional (Lean.Parser.atomic (Lean.Parser.symbol ":") >> Lean.Parser.termParser Lean.Parser.maxPrec)

def Lean.Parser.Term.withAnonymousAntiquot : Parser

Equations

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

def Lean.Parser.Term.leading_parser : Parser

Equations

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

def Lean.Parser.Term.trailing_parser : Parser

Equations

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

def Lean.Parser.Term.borrowed : Parser

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/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=ffi-borrowing for a complete description.

Equations

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

def Lean.Parser.Term.quotedName : Parser

A literal of type Name.

Equations

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

def Lean.Parser.Term.doubleQuotedName : Parser

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.

def Lean.Parser.Term.posConfigItem : Parser

+opt is short for (opt := true). It sets the opt configuration option to true.

Equations

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

def Lean.Parser.Term.negConfigItem : Parser

-opt is short for (opt := false). It sets the opt configuration option to false.

Equations

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

def Lean.Parser.Term.valConfigItem : Parser

(opt := val) sets the opt configuration option to val.

As a special case, (config := ...) sets the entire configuration.

Equations

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

def Lean.Parser.Term.configItem : Parser

A configuration item.

Equations

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

def Lean.Parser.Term.optConfig : Parser

Configuration options for tactics, commands, and other elaborators.

Equations

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

def Lean.Parser.Term.letId : Parser

Equations

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

def Lean.Parser.Term.letIdBinder : Parser

Equations

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

def Lean.Parser.Term.letIdLhs : Parser

Equations

• Lean.Parser.Term.letIdLhs = Lean.Parser.Term.letId >> Lean.Parser.many (Lean.Parser.ppSpace >> Lean.Parser.Term.letIdBinder) >> Lean.Parser.Term.optType

def Lean.Parser.Term.letIdDecl : Parser

Equations

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

def Lean.Parser.Term.letPatDecl (requireParens : Bool := false) : Parser

Equations

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

def Lean.Parser.Term.letEqnsDecl : Parser

Equations

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

def Lean.Parser.Term.letDecl : Parser

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.

def Lean.Parser.Term.letOptNondep : Parser

+nondep elaborates as a nondependent let, a have expression.

Equations

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

def Lean.Parser.Term.letOptPostponeValue : Parser

+postponeValue causes the body of the let to be elaborated before the value.

Equations

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

def Lean.Parser.Term.letOptUsedOnly : Parser

+usedOnly causes unused lets bindings to be eliminated.

Equations

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

def Lean.Parser.Term.letOptZeta : Parser

+zeta immediately inlines the let value after elaboration (it zeta reduces the let).

Equations

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

def Lean.Parser.Term.letOptGeneralize : Parser

+generalize directs let/have to generalize the value from the expected type before elaborating the body.

Equations

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

def Lean.Parser.Term.letOpts : Parser

Equations

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

def Lean.Parser.Term.letPosOpt : Parser

Equations

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

def Lean.Parser.Term.letNegOpt : Parser

Equations

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

def Lean.Parser.Term.letOptEq : Parser

let (eq := h) x := v; ... adds the equality h : x = v to the context while elaborating the body.

Equations

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

def Lean.Parser.Term.letConfigItem : Parser

Equations

• Lean.Parser.Term.letConfigItem = (Lean.Parser.Term.letPosOpt <|> Lean.Parser.Term.letNegOpt <|> Lean.Parser.Term.letOptEq)

def Lean.Parser.Term.letConfig : Parser

Configuration options for let tactics.

Equations

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

def Lean.Parser.Term.let : Parser

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

The anaphoric let let := v defines a variable called this.

Equations

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

def Lean.Parser.Term.have : Parser

have is used to declare local hypotheses and opaque local definitions.

It has the same syntax as let, and it is equivalent to let +nondep, creating a nondependent let expression.

Equations

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

def Lean.Parser.Term.let_fun : Parser

let_fun x := v; b is deprecated syntax sugar for have x := v; b.

Equations

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

def Lean.Parser.Term.let_delayed : Parser

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.

def Lean.Parser.Term.let_tmp : Parser

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.

def Lean.Parser.Term.haveI : Parser

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

Equations

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

def Lean.Parser.Term.letI : Parser

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

Equations

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

def Lean.Parser.Term.scoped : Parser

Equations

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

def Lean.Parser.Term.local : Parser

Equations

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

def Lean.Parser.Term.attrKind : Parser

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

Equations

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

def Lean.Parser.Term.attrInstance : Parser

Equations

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

def Lean.Parser.Term.attributes : Parser

Equations

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

def Lean.Parser.Termination.terminationBy : Parser

Specify a termination measure 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) : Nat → Nat → Nat :=
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 measure will be inferred. If written as termination_by?, the inferred termination measure will be suggested.

Equations

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

def Lean.Parser.Termination.terminationBy? : Parser

Specify a termination measure 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) : Nat → Nat → Nat :=
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 measure will be inferred. If written as termination_by?, the inferred termination measure will be suggested.

Equations

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

def Lean.Parser.Termination.partialFixpoint : Parser

Defines a possibly non-terminating function as a fixed-point in a suitable partial order.

Such a function is compiled as if it was marked partial, but its equations are provided as theorems, so that it can be verified.

In general it accepts functions whose return type has a Lean.Order.CCPO instance and whose definition is Lean.Order.monotone with regard to its recursive calls.

Common special cases are

• Functions whose type is inhabited a-priori (as with partial), and where all recursive calls are in tail-call position.
• Monadic in certain “monotone chain-complete monads” (in particular, Option) composed using the bind operator and other supported monadic combinators.

By default, the monotonicity proof is performed by the compositional monotonicity tactic. Using the syntax partial_fixpoint monotonicity by $tac the proof can be done manually.

Equations

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

def Lean.Parser.Termination.coinductiveFixpoint : Parser

Defines a coinductive predicate using lattice theory, based on the Knaster-Tarski fixpoint theorem.

This feature constructs coinductive predicates by leveraging the lattice structure on Prop and ensures correctness through monotonicity.

The coinductive predicate is defined as the greatest fixed point of a monotone function on Prop.

By default, monotonicity is verified automatically. However, users can provide custom proofs of monotonicity if needed.

Equations

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

def Lean.Parser.Termination.inductiveFixpoint : Parser

Defines an inductive predicate using lattice theory, based on the Knaster-Tarski fixpoint theorem.

This feature constructs inductive predicates by leveraging the lattice structure on Prop and ensures correctness through monotonicity.

The inductive predicate is defined as the least fixed point of a monotone function on Prop.

By default, monotonicity is verified automatically. However, users can provide custom proofs of monotonicity if needed.

Equations

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

def Lean.Parser.Termination.decreasingBy : Parser

Manually prove that the termination measure (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.

def Lean.Parser.Termination.suffix : Parser

Termination hints are termination_by and decreasing_by, in that order.

Equations

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

def Lean.Parser.Term.letRecDecl : Parser

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.

def Lean.Parser.Term.letRecDecls : Parser

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.

def Lean.Parser.Term.letrec : Parser

Equations

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

def Lean.Parser.Term.whereFinallySubsection : Parser

A named subsection of where ... finally. In the future, sections such as decreasing_by might become syntactic sugar for an where ... finally subsection | decreasing => ....

Equations

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

def Lean.Parser.Term.whereFinally : Parser

The finally section trailing a where opens a tactic block to fill in ?holes in the definition body.

Equations

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

def Lean.Parser.Term.whereDecls : Parser

Equations

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

def Lean.Parser.Term.matchAltsWhereDecls : Parser

Equations

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

def Lean.Parser.Term.noindex : Parser

Equations

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

def Lean.Parser.Term.unsafe : Parser

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.

def Lean.Parser.Term.binrel : Parser

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.

def Lean.Parser.Term.binrel_no_prop : Parser

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.

def Lean.Parser.Term.binop : Parser

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.

def Lean.Parser.Term.binop_lazy : Parser

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.

def Lean.Parser.Term.leftact : Parser

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.

def Lean.Parser.Term.rightact : Parser

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.

def Lean.Parser.Term.unop : Parser

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.

def Lean.Parser.Term.forInMacro : Parser

Equations

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

def Lean.Parser.Term.forInMacro' : Parser

Equations

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

def Lean.Parser.Term.declName : Parser

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.

def Lean.Parser.Term.privateDecl : Parser

private_decl% e elaborates e in a private context and wraps the result in a helper def.

Equations

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

def Lean.Parser.Term.withDeclName : Parser

• 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.

def Lean.Parser.Term.typeOf : Parser

Equations

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

def Lean.Parser.Term.ensureTypeOf : Parser

Equations

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

def Lean.Parser.Term.ensureExpectedType : Parser

Equations

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

def Lean.Parser.Term.noImplicitLambda : Parser

Equations

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

def Lean.Parser.Term.inferInstanceAs : Parser

inferInstanceAs α synthesizes an instance of type α and then adjusts it to conform to the expected type β, which must be inferable from context.

Example:

def D := Nat
instance : Inhabited D := inferInstanceAs (Inhabited Nat)

The adjustment will make sure that when the resulting instance will not "leak" the RHS Nat when reduced at transparency levels below semireducible, i.e. where D would not be unfolded either, preventing "defeq abuse".

More specifically, given the "source type" (the argument) and "target type" (the expected type), inferInstanceAs synthesizes an instance for the source type and then unfolds and rewraps its components (fields, nested instances) as necessary to make them compatible with the target type. The individual steps are represented by the following options, which all default to enabled and can be disabled to help with porting:

• backward.inferInstanceAs.wrap: master switch for instance adjustment in both inferInstanceAs and the default deriving handler
• backward.inferInstanceAs.wrap.reuseSubInstances: reuse existing instances for the target type for sub-instance fields to avoid non-defeq instance diamonds
• backward.inferInstanceAs.wrap.instances: wrap non-reducible instances in auxiliary definitions
• backward.inferInstanceAs.wrap.data: wrap data fields in auxiliary definitions (proof fields are always wrapped)

If you just need to synthesize an instance without transporting between types, use inferInstance instead, potentially with a type annotation for the expected type.

Equations

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

def Lean.Parser.Term.valueOf : Parser

value_of% x elaborates to the value of x, which can be a local or global definition.

Equations

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

def Lean.Parser.Term.clear : Parser

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.

def Lean.Parser.Term.letMVar : Parser

Equations

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

def Lean.Parser.Term.waitIfTypeMVar : Parser

Equations

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

def Lean.Parser.Term.waitIfTypeContainsMVar : Parser

Equations

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

def Lean.Parser.Term.waitIfContainsMVar : Parser

Equations

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

def Lean.Parser.Term.waitForExpectedType : Parser

wait_for_expected_type% e elaborates e against its expected type, postponing while that type is an unassigned metavariable so an outParam determined by instance synthesis is resolved first.

Equations

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

def Lean.Parser.Term.defaultOrOfNonempty : Parser

Equations

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

def Lean.Parser.Term.noErrorIfUnused : Parser

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.

def Lean.Parser.Term.contractEPosts : Parser

contract_eposts% e unfolds the EPostSlot.set applications and ⊥ in e, e.g. to an estack⟨...⟩ expression. Used in the expansion of throws clauses of a def contract to yield simpler specs.

Equations

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

def Lean.Parser.Term.namedArgument : Parser

Equations

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

def Lean.Parser.Term.ellipsis : Parser

In a function application, .. notation inserts zero or more _ placeholders.

Equations

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

def Lean.Parser.Term.argument : Parser

Equations

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

def Lean.Parser.Term.app : TrailingParser

Equations

• Lean.Parser.Term.app = Lean.Parser.trailingNode `Lean.Parser.Term.app Lean.Parser.leadPrec Lean.Parser.maxPrec (Lean.Parser.many1 Lean.Parser.Term.argument)

def Lean.Parser.Term.proj : TrailingParser

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.

def Lean.Parser.Term.completion : TrailingParser

Equations

• Lean.Parser.Term.completion = Lean.Parser.trailingNode `Lean.Parser.Term.completion 1024 0 (Lean.Parser.checkNoWsBefore >> Lean.Parser.symbol ".")

def Lean.Parser.Term.arrow : TrailingParser

Equations

• Lean.Parser.Term.arrow = Lean.Parser.trailingNode `Lean.Parser.Term.arrow 1024 0 (Lean.Parser.checkPrec 25 >> Lean.Parser.unicodeSymbol " → " " -> " >> Lean.Parser.termParser 25)

def Lean.Parser.Term.identProjKind : Name

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

• Lean.Parser.Term.identProjKind = `Lean.Parser.Term.identProj

def Lean.Parser.Term.dotIdent : Parser

Equations

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

def Lean.Parser.Term.isIdent (stx : Syntax) : Bool

Equations

• Lean.Parser.Term.isIdent stx = (stx.isAntiquot || stx.isIdent)

def Lean.Parser.Term.isIdentOrDotIdentOrProj (stx : Syntax) : Bool

Predicate for what explicitUniv can follow. It is only meant to be used on an identifier that becomes the head constant of an application.

Equations

• Lean.Parser.Term.isIdentOrDotIdentOrProj stx = (Lean.Parser.Term.isIdent stx || stx.isOfKind `Lean.Parser.Term.dotIdent || stx.isOfKind `Lean.Parser.Term.proj)

def Lean.Parser.Term.explicitUnivSuffix : Parser

Syntax for .{u, ...} itself. Generally the explicitUniv trailing parser suffices. However, for e |>.x.{u} a1 a2 a3 notation we need to be able to express explicit universes in the middle of the syntax.

Equations

• Lean.Parser.Term.explicitUnivSuffix = Lean.Parser.checkNoWsBefore "no space before '.{'" >> Lean.Parser.symbol ".{" >> Lean.Parser.sepBy1 Lean.Parser.levelParser ", " >> Lean.Parser.symbol "}"

def Lean.Parser.Term.explicitUniv : TrailingParser

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

Equations

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

def Lean.Parser.Term.namedPattern : TrailingParser

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.

def Lean.Parser.Term.pipeProj : TrailingParser

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.

def Lean.Parser.Term.pipeCompletion : TrailingParser

Equations

• Lean.Parser.Term.pipeCompletion = Lean.Parser.trailingNode `Lean.Parser.Term.pipeCompletion Lean.Parser.minPrec 0 (Lean.Parser.symbol " |>.")

def Lean.Parser.Term.subst : TrailingParser

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

• Lean.Parser.Term.subst = Lean.Parser.trailingNode `Lean.Parser.Term.subst 75 0 (Lean.Parser.symbol " ▸ " >> Lean.Parser.termParser 75)

def Lean.Parser.Term.bracketedBinderF : Parser

Equations

• Lean.Parser.Term.bracketedBinderF = Lean.Parser.Term.bracketedBinder

@[instance_reducible]

instance Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_lean_1 : Coe (TSyntax `Lean.Parser.Term.bracketedBinderF) (TSyntax `Lean.Parser.Term.bracketedBinder)

Equations

• Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_lean_1 = { coe := fun (s : Lean.TSyntax `Lean.Parser.Term.bracketedBinderF) => { raw := s.raw } }

def Lean.Parser.Term.panic : Parser

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.

def Lean.Parser.Term.unreachable : Parser

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

Equations

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

def Lean.Parser.Term.dbgTrace : Parser

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.

def Lean.Parser.Term.idbg : Parser

Term-level form of the interactive debugger. See the doIdbg do element for full documentation.

Equations

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

def Lean.Parser.Term.assert : Parser

assert! cond panics if cond evaluates to false.

Equations

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

def Lean.Parser.Term.debugAssert : Parser

debug_assert! cond panics if cond evaluates to false and the executing code has been built with debug assertions enabled (see the debugAssertions option).

Equations

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

def Lean.Parser.Term.macroArg : Parser

Equations

• Lean.Parser.Term.macroArg = Lean.Parser.termParser Lean.Parser.maxPrec

def Lean.Parser.Term.macroDollarArg : Parser

Equations

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

def Lean.Parser.Term.macroLastArg : Parser

Equations

• Lean.Parser.Term.macroLastArg = (Lean.Parser.Term.macroDollarArg <|> Lean.Parser.Term.macroArg)

def Lean.Parser.Term.stateRefT : Parser

A state monad that uses an actual mutable reference cell (i.e. an ST.Ref).

This is syntax, rather than a function, to make it easier to use. Its elaborator synthesizes an appropriate parameter for the underlying monad's ST effects, then passes it to StateRefT'.

Equations

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

def Lean.Parser.Term.dynamicQuot : Parser

Equations

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

def Lean.Parser.Term.showTermElabImpl : Parser

Implementation of the show_term term elaborator.

Equations

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

match_expr support.

def Lean.Parser.Term.matchExprPat : Parser

Equations

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

def Lean.Parser.Term.matchExprAlt (rhsParser : Parser) : Parser

Equations

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

def Lean.Parser.Term.matchExprElseAlt (rhsParser : Parser) : Parser

Equations

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

def Lean.Parser.Term.matchExprAlts (rhsParser : Parser) : Parser

Equations

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

def Lean.Parser.Term.matchExprAltExpr : Parser

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

Equations

• Lean.Parser.Term.matchExprAltExpr = Lean.Parser.Term.matchExprAlt Lean.Parser.termParser

@[instance_reducible]

instance Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_lean_2 : Coe (TSyntax `Lean.Parser.Term.matchExprAltExpr) (TSyntax `Lean.Parser.Term.matchExprAlt)

Equations

• Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil_lean_2 = { coe := fun (stx : Lean.TSyntax `Lean.Parser.Term.matchExprAltExpr) => { raw := stx.raw } }

def Lean.Parser.Term.matchExpr : Parser

Equations

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

def Lean.Parser.Term.letExpr : Parser

Equations

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

def Lean.Parser.Term.throwNamedErrorMacro : Parser

Throws an error exception, tagging the associated message as a named error with the specified name and validating that an associated error explanation exists. The message may be passed as an interpolated string or a MessageData term. The result of getRef is used as position information.

Equations

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

def Lean.Parser.Term.throwNamedErrorAtMacro : Parser

Throws an error exception, tagging the associated message as a named error with the specified name and validating that an associated error explanation exists. The error name must be followed by a Syntax at which the error is to be thrown. The message is the final argument and may be passed as an interpolated string or a MessageData term.

Equations

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

def Lean.Parser.Term.logNamedErrorMacro : Parser

Logs an error, tagging the message as a named error with the specified name and validating that an associated error explanation exists. The message may be passed as an interpolated string or a MessageData term. The result of getRef is used as position information.

Equations

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

def Lean.Parser.Term.logNamedErrorAtMacro : Parser

Logs an error, tagging the message as a named error with the specified name and validating that an associated error explanation exists. The error name must be followed by a Syntax at which the error is to be logged. The message is the final argument and may be passed as an interpolated string or a MessageData term.

Equations

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

def Lean.Parser.Term.logNamedWarningMacro : Parser

Logs a warning, tagging the message as a named diagnostic with the specified name and validating that an associated error explanation exists. The message may be passed as an interpolated string or a MessageData term. The result of getRef is used as position information.

Equations

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

def Lean.Parser.Term.logNamedWarningAtMacro : Parser

Logs a warning, tagging the message as a named diagnostic with the specified name and validating that an associated error explanation exists. The error name must be followed by a Syntax at which the warning is to be logged. The message is the final argument and may be passed as an interpolated string or a MessageData term.

Equations

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

def Lean.Parser.Term.mdataDiagnostic : Parser

Representation of an expression with metadata used during pretty printing for the pp.mdata option.

Equations

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

def Lean.Parser.Tactic.quot : Parser

Equations

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

def Lean.Parser.Tactic.quotSeq : Parser

Equations

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