source
def Lean.Parser.Command.versoCommentBodyFn :
ParserFn
Equations

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

Instances For

source
def Lean.Parser.Command.versoCommentBody :
Parser
Equations

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

Instances For

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

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

Instances For

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

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

Instances For

source
def Lean.Parser.Command.commentBody :
Parser
Equations

- Lean.Parser.Command.commentBody = { fn := Lean.Parser.rawFn (Lean.Parser.finishCommentBlock true 1) true }

Instances For

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

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

Instances For

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

- Lean.Parser.Command.commentBody.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.Name.anonymous

Instances For

source
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 the remainder of the comment, `foo -/` in this example. Use `TSyntax.getDocString` to extract the body 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.

Instances For

source
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 the remainder of the comment, `foo -/` in this example. Use `TSyntax.getDocString` to extract the body 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

Instances For

source
def Lean.Parser.darrow :
Parser
Equations

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

Instances For

source
def Lean.Parser.semicolonOrLinebreak :
Parser
Equations

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

Instances For

# Built-in parsers #

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

Instances For

source
def Lean.Parser.Term.byTactic' :
Parser
Equations

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

Instances For

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

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

Instances For

source
def Lean.Parser.Term.ident :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.num :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.scientific :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.str :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.char :
Parser
Equations

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
def Lean.Parser.Term.hygienicLParen :
Parser
Equations

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
def Lean.Parser.Term.fromTerm :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.showRhs :
Parser
Equations

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

Instances For

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

Instances For

source
def Lean.Parser.Term.suffices :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.show :
Parser
Equations

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

Instances For

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

Instances For

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

Instances For

source
def Lean.Parser.Term.depArrow :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.forall :
Parser
Equations

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

Instances For

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

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

Instances For

source
def Lean.Parser.Term.matchAltExpr :
Parser

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

Equations

- Lean.Parser.Term.matchAltExpr = Lean.Parser.Term.matchAlt

Instances For

source
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 } }

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

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

Instances For

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

Instances For

source
def Lean.Parser.Term.trueVal :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.falseVal :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.generalizingParam :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.motive :
Parser
Equations

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

Instances For

source
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.atom`s 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

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

Instances For

source
def Lean.Parser.Term.nofun :
Parser
Equations

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

Instances For

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

Instances For

source
def Lean.Parser.Term.structInstFieldDef :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.structInstFieldEqns :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.funImplicitBinder :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.funStrictImplicitBinder :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.funBinder :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.basicFun :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.fun :
Parser
Equations

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

Instances For

source
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)

Instances For

source
def Lean.Parser.Term.withAnonymousAntiquot :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.leading_parser :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.trailing_parser :
Parser
Equations

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

Instances For

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

Instances For

source
def Lean.Parser.Term.quotedName :
Parser

A literal of type `Name`.

Equations

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

Instances For

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

Instances For

source
def Lean.Parser.Term.letId :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.letIdBinder :
Parser
Equations

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

Instances For

source
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

Instances For

source
def Lean.Parser.Term.letIdDecl :
Parser
Equations

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

Instances For

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

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

Instances For

source
def Lean.Parser.Term.letEqnsDecl :
Parser
Equations

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
def Lean.Parser.Term.letOptUsedOnly :
Parser

`+usedOnly` causes unused `let`s bindings to be eliminated.

Equations

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

Instances For

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

Instances For

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

Instances For

source
def Lean.Parser.Term.letOpts :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.letPosOpt :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.letNegOpt :
Parser
Equations

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

Instances For

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

Instances For

source
def Lean.Parser.Term.letConfigItem :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.letConfig :
Parser

Configuration options for `let` tactics.

Equations

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
def Lean.Parser.Term.scoped :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.local :
Parser
Equations

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

Instances For

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

Instances For

source
def Lean.Parser.Term.attrInstance :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.attributes :
Parser
Equations

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
def Lean.Parser.Term.letrec :
Parser
Equations

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

Instances For

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

Instances For

source
def Lean.Parser.Term.whereFinally :
Parser

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

Equations

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

Instances For

source
def Lean.Parser.Term.whereDecls :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.matchAltsWhereDecls :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.noindex :
Parser
Equations

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
def Lean.Parser.Term.forInMacro :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.forInMacro' :
Parser
Equations

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
def Lean.Parser.Term.typeOf :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.ensureTypeOf :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.ensureExpectedType :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.noImplicitLambda :
Parser
Equations

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

Instances For

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

Instances For

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

Instances For

source
def Lean.Parser.Term.letMVar :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.waitIfTypeMVar :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.waitIfTypeContainsMVar :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.waitIfContainsMVar :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.defaultOrOfNonempty :
Parser
Equations

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

Instances For

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

Instances For

source
def Lean.Parser.Term.namedArgument :
Parser
Equations

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

Instances For

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

Instances For

source
def Lean.Parser.Term.argument :
Parser
Equations

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

Instances For

source
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)

Instances For

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

Instances For

source
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 ".")

Instances For

source
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)

Instances For

source
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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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 " |>.")

Instances For

source
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.sepBy1 (Lean.Parser.termParser 75) " ▸ ")

Instances For

source
def Lean.Parser.Term.bracketedBinderF :
Parser
Equations

- Lean.Parser.Term.bracketedBinderF = Lean.Parser.Term.bracketedBinder

Instances For

source
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 } }

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
def Lean.Parser.Term.macroArg :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.macroDollarArg :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.macroLastArg :
Parser
Equations

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

Instances For

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

Instances For

source
def Lean.Parser.Term.dynamicQuot :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.dotIdent :
Parser
Equations

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

Instances For

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

Instances For

`match_expr` support.

source
def Lean.Parser.Term.matchExprPat :
Parser
Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
def Lean.Parser.Term.matchExpr :
Parser
Equations

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

Instances For

source
def Lean.Parser.Term.letExpr :
Parser
Equations

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
def Lean.Parser.Tactic.quot :
Parser
Equations

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

Instances For

source
def Lean.Parser.Tactic.quotSeq :
Parser
Equations

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

Instances For