def Lean.Parser.Command.commentBody : Lean.Parser.Parser

Equations

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

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

Equations

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

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

Equations

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

def Lean.Parser.Command.docComment : Lean.Parser.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.

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

Equations

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

@[inline]

def Lean.Parser.tacticParser (rbp : optParam Nat 0) : Lean.Parser.Parser

Equations

• Lean.Parser.tacticParser rbp = Lean.Parser.categoryParser `tactic rbp

@[inline]

def Lean.Parser.convParser (rbp : optParam Nat 0) : Lean.Parser.Parser

Equations

• Lean.Parser.convParser rbp = Lean.Parser.categoryParser `conv rbp

def Lean.Parser.Tactic.sepByIndentSemicolon (p : Lean.Parser.Parser) : Lean.Parser.Parser

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

example := by
  skip
  skip

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

Equations

• Lean.Parser.Tactic.sepByIndentSemicolon p = Lean.Parser.sepByIndent p "; " (Lean.Parser.symbol "; ") true

def Lean.Parser.Tactic.sepBy1IndentSemicolon (p : Lean.Parser.Parser) : Lean.Parser.Parser

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

example := by
  skip
  skip

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

Equations

• Lean.Parser.Tactic.sepBy1IndentSemicolon p = Lean.Parser.sepBy1Indent p "; " (Lean.Parser.symbol "; ") true

def Lean.Parser.Tactic.tacticSeq1Indented : Lean.Parser.Parser

Equations

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

def Lean.Parser.Tactic.tacticSeqBracketed : Lean.Parser.Parser

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

Equations

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

def Lean.Parser.Tactic.tacticSeq : Lean.Parser.Parser

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

Equations

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

def Lean.Parser.Tactic.tacticSeqIndentGt : Lean.Parser.Parser

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

Equations

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

def Lean.Parser.Tactic.seq1 : Lean.Parser.Parser

Equations

• Lean.Parser.Tactic.seq1 = Lean.Parser.node `Lean.Parser.Tactic.seq1 (Lean.Parser.sepBy1 Lean.Parser.tacticParser ";\n" (Lean.Parser.symbol ";\n") true)

def Lean.Parser.darrow : Lean.Parser.Parser

Equations

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

def Lean.Parser.semicolonOrLinebreak : Lean.Parser.Parser

Equations

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

def Lean.Parser.Termination.terminationBy : Lean.Parser.Parser

Specify a termination argument for well-founded termination:

termination_by a - b

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

If the fuction 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

If omitted, a termination argument will be inferred.

Equations

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

def Lean.Parser.Termination.decreasingBy : Lean.Parser.Parser

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

By default, the tactic decreasing_tactic is used.

Equations

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

def Lean.Parser.Termination.suffix : Lean.Parser.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.

Built-in parsers

def Lean.Parser.Term.byTactic : Lean.Parser.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' : Lean.Parser.Parser

Equations

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

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

Equations

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

def Lean.Parser.Term.ident : Lean.Parser.Parser

Equations

• Lean.Parser.Term.ident = HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.maxPrec) fun (x : Unit) => Lean.Parser.ident

def Lean.Parser.Term.num : Lean.Parser.Parser

Equations

• Lean.Parser.Term.num = HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.maxPrec) fun (x : Unit) => Lean.Parser.numLit

def Lean.Parser.Term.scientific : Lean.Parser.Parser

Equations

• Lean.Parser.Term.scientific = HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.maxPrec) fun (x : Unit) => Lean.Parser.scientificLit

def Lean.Parser.Term.str : Lean.Parser.Parser

Equations

• Lean.Parser.Term.str = HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.maxPrec) fun (x : Unit) => Lean.Parser.strLit

def Lean.Parser.Term.char : Lean.Parser.Parser

Equations

• Lean.Parser.Term.char = HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.maxPrec) fun (x : Unit) => Lean.Parser.charLit

def Lean.Parser.Term.type : Lean.Parser.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 : Lean.Parser.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 : Lean.Parser.Parser

The universe of propositions. Prop ≡ Sort 0.

Equations

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

def Lean.Parser.Term.hole : Lean.Parser.Parser

A placeholder term, to be synthesized by unification.

Equations

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

def Lean.Parser.Term.syntheticHole : Lean.Parser.Parser

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

Equations

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

def Lean.Parser.Term.binderIdent : Lean.Parser.Parser

Equations

• Lean.Parser.Term.binderIdent = HOrElse.hOrElse Lean.Parser.Term.ident fun (x : Unit) => Lean.Parser.Term.hole

def Lean.Parser.Term.sorry : Lean.Parser.Parser

A temporary placeholder for a missing proof or value.

Equations

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

def Lean.Parser.Term.cdot : Lean.Parser.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.

Equations

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

def Lean.Parser.Term.typeAscription : Lean.Parser.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 : Lean.Parser.Parser

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

Equations

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

def Lean.Parser.Term.paren : Lean.Parser.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)

Equations

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

def Lean.Parser.Term.anonymousCtor : Lean.Parser.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.optIdent : Lean.Parser.Parser

Equations

• Lean.Parser.Term.optIdent = Lean.Parser.optional (Lean.Parser.atomic (HAndThen.hAndThen Lean.Parser.Term.ident fun (x : Unit) => Lean.Parser.symbol " : "))

def Lean.Parser.Term.fromTerm : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.showRhs : Lean.Parser.Parser

Equations

• Lean.Parser.Term.showRhs = HOrElse.hOrElse Lean.Parser.Term.fromTerm fun (x : Unit) => Lean.Parser.Term.byTactic'

def Lean.Parser.Term.sufficesDecl : Lean.Parser.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 : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.show : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.structInstArrayRef : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.structInstLVal : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.structInstField : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.structInstFieldAbbrev : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.optEllipsis : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.structInst : Lean.Parser.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.typeSpec : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.optType : Lean.Parser.Parser

Equations

• Lean.Parser.Term.optType = Lean.Parser.optional Lean.Parser.Term.typeSpec

def Lean.Parser.Term.explicit : Lean.Parser.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 : Lean.Parser.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.binderType (requireType : optParam Bool false) : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.binderTactic : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.binderDefault : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.binderDefault.parenthesizer : Lean.PrettyPrinter.Parenthesizer

Equations

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

def Lean.Parser.Term.explicitBinder (requireType : optParam Bool false) : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.implicitBinder (requireType : optParam Bool false) : Lean.Parser.Parser

Implicit binder. In regular applications without @, it is automatically inserted and solved by unification whenever all explicit parameters before it are specified.

Equations

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

def Lean.Parser.Term.strictImplicitLeftBracket : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.strictImplicitRightBracket : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.strictImplicitBinder (requireType : optParam Bool false) : Lean.Parser.Parser

Strict-implicit binder. In contrast to { ... } regular implicit binders, a strict-implicit binder is inserted automatically only when at least one subsequent explicit parameter is specified.

Equations

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

def Lean.Parser.Term.instBinder : Lean.Parser.Parser

Instance-implicit binder. In regular applications without @, it is automatically inserted and solved by typeclass inference of the specified class.

Equations

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

def Lean.Parser.Term.bracketedBinder (requireType : optParam Bool false) : Lean.Parser.Parser

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

• An explicit binder like (x y : A)
• An implicit binder like {x y : A}
• A strict implicit binder, ⦃y z : A⦄ or its ASCII alternative {{y z : A}}
• An instance binder [A] or [x : A] (multiple variables are not allowed here)

Equations

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

def Lean.Parser.Term.depArrow : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.forall : Lean.Parser.Parser

Equations

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

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

Equations

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

def Lean.Parser.Term.matchAltExpr : Lean.Parser.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 Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStr4Nil : Coe (Lean.TSyntax `Lean.Parser.Term.matchAltExpr) (Lean.TSyntax `Lean.Parser.Term.matchAlt)

Equations

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

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

Equations

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

def Lean.Parser.Term.matchDiscr : Lean.Parser.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 : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.falseVal : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.generalizingParam : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.motive : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.match : Lean.Parser.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 : Lean.Parser.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.funImplicitBinder : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.funStrictImplicitBinder : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.funBinder : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.basicFun : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.fun : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.optExprPrecedence : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.withAnonymousAntiquot : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.leading_parser : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.trailing_parser : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.borrowed : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.quotedName : Lean.Parser.Parser

A literal of type Name.

Equations

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

def Lean.Parser.Term.doubleQuotedName : Lean.Parser.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.letIdBinder : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.letIdLhs : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.letIdDecl : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.letPatDecl : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.letEqnsDecl : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.letDecl : Lean.Parser.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.let : Lean.Parser.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

Equations

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

def Lean.Parser.Term.let_fun : Lean.Parser.Parser

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

Equations

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

def Lean.Parser.Term.let_delayed : Lean.Parser.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 : Lean.Parser.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.haveIdLhs : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.haveIdDecl : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.haveEqnsDecl : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.haveDecl : Lean.Parser.Parser

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

Equations

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

def Lean.Parser.Term.have : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.scoped : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.local : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.attrKind : Lean.Parser.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 : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.attributes : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.letRecDecl : Lean.Parser.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 : Lean.Parser.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 : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.whereDecls : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.matchAltsWhereDecls : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.noindex : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.binrel : Lean.Parser.Parser

binrel% r a b elaborates r a b as a binary relation using the type propogation 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 : Lean.Parser.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 : Lean.Parser.Parser

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

Equations

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

def Lean.Parser.Term.binop_lazy : Lean.Parser.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 : Lean.Parser.Parser

leftact% f a b elaborates f a b as a left action using the type propogation 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 : Lean.Parser.Parser

rightact% f a b elaborates f a b as a right action using the type propogation 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 : Lean.Parser.Parser

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

Equations

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

def Lean.Parser.Term.forInMacro : Lean.Parser.Parser

Equations

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

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

Equations

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

def Lean.Parser.Term.declName : Lean.Parser.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.withDeclName : Lean.Parser.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 : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.ensureTypeOf : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.ensureExpectedType : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.noImplicitLambda : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.clear : Lean.Parser.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 : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.waitIfTypeMVar : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.waitIfTypeContainsMVar : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.waitIfContainsMVar : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.defaultOrOfNonempty : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.noErrorIfUnused : Lean.Parser.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.namedArgument : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.ellipsis : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.argument : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.app : Lean.Parser.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 : Lean.Parser.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 : Lean.Parser.TrailingParser

Equations

• Lean.Parser.Term.completion = Lean.Parser.trailingNode `Lean.Parser.Term.completion 1024 0 (HAndThen.hAndThen Lean.Parser.checkNoWsBefore fun (x : Unit) => Lean.Parser.symbol ".")

def Lean.Parser.Term.arrow : Lean.Parser.TrailingParser

Equations

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

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

Equations

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

def Lean.Parser.Term.explicitUniv : Lean.Parser.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 : Lean.Parser.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 : Lean.Parser.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 : Lean.Parser.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 : Lean.Parser.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. See the Chapter "Quantifiers and Equality" in the manual "Theorem Proving in Lean" for additional information.

Equations

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

def Lean.Parser.Term.bracketedBinderF : Lean.Parser.Parser

Equations

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

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

Equations

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

def Lean.Parser.Term.panic : Lean.Parser.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 : Lean.Parser.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 : Lean.Parser.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.assert : Lean.Parser.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.macroArg : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.macroDollarArg : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.macroLastArg : Lean.Parser.Parser

Equations

• Lean.Parser.Term.macroLastArg = HOrElse.hOrElse Lean.Parser.Term.macroDollarArg fun (x : Unit) => Lean.Parser.Term.macroArg

def Lean.Parser.Term.stateRefT : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.dynamicQuot : Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.dotIdent : Lean.Parser.Parser

Equations

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

def Lean.Parser.Tactic.quot : Lean.Parser.Parser

Equations

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

def Lean.Parser.Tactic.quotSeq : Lean.Parser.Parser

Equations

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