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.
Instances For
Instances For
sepByIndentSemicolon(p)
parses a sequence of p
optionally followed by ;
,
similar to manyIndent(p ";"?)
, except that if two occurrences of p
occur on the same line,
the ;
is mandatory. This is used by tactic parsing, so that
example := by
skip
skip
is legal, but by skip skip
is not - it must be written as by skip; skip
.
Instances For
sepBy1IndentSemicolon(p)
parses a (nonempty) sequence of p
optionally followed by ;
,
similar to many1Indent(p ";"?)
, except that if two occurrences of p
occur on the same line,
the ;
is mandatory. This is used by tactic parsing, so that
example := by
skip
skip
is legal, but by skip skip
is not - it must be written as by skip; skip
.
Instances For
The syntax { tacs }
is an alternative syntax for · tacs
.
It runs the tactics in sequence, and fails if the goal is not solved.
Instances For
A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics. Delimiter-free indentation is determined by the first tactic of the sequence.
Instances For
Same as [tacticSeq
] but requires delimiter-free tactic sequence to have strict indentation.
The strict indentation requirement only apply to nested by
s, as top-level by
s do not have a
position set.
Instances For
Built-in parsers #
by tac
constructs a term of the expected type by running the tactic(s) tac
.
Instances For
A type universe. Type ≡ Type 0
, Type u ≡ Sort (u + 1)
.
Instances For
A specific universe in Lean's infinite hierarchy of universes.
Instances For
The universe of propositions. Prop ≡ Sort 0
.
Instances For
A placeholder term, to be synthesized by unification.
Instances For
Parses a "synthetic hole", that is, ?foo
or ?_
.
This syntax is used to construct named metavariables.
Instances For
A temporary placeholder for a missing proof or value.
Instances For
A placeholder for an implicit lambda abstraction's variable. The lambda abstraction is scoped to the surrounding parentheses.
For example, (· + ·)
is equivalent to fun x y => x + y
.
Instances For
Type ascription notation: (0 : Int)
instructs Lean to process 0
as a value of type Int
.
An empty type ascription (e :)
elaborates e
without the expected type.
This is occasionally useful when Lean's heuristics for filling arguments from the expected type
do not yield the right result.
Instances For
Parentheses, used for grouping expressions (e.g., a * (b + c)
).
Can also be used for creating simple functions when combined with ·
. Here are some examples:
(· + 1)
is shorthand forfun x => x + 1
(· + ·)
is shorthand forfun x y => x + y
(f · a b)
is shorthand forfun x => f x a b
(h (· + 1) ·)
is shorthand forfun x => h (fun y => y + 1) x
- also applies to other parentheses-like notations such as
(·, 1)
Instances For
The anonymous constructor ⟨e, ...⟩
is equivalent to c e ...
if the
expected type is an inductive type with a single constructor c
.
If more terms are given than c
has parameters, the remaining arguments
are turned into a new anonymous constructor application. For example,
⟨a, b, c⟩ : α × (β × γ)
is equivalent to ⟨a, ⟨b, c⟩⟩
.
Instances For
A sufficesDecl
represents everything that comes after the suffices
keyword:
an optional x :
, then a term ty
, then from val
or by tac
.
Instances For
Structure instance. { x := e, ... }
assigns e
to field x
, which may be
inherited. If e
is itself a variable called x
, it can be elided:
fun y => { x := 1, y }
.
A structure update of an existing value can be given via with
:
{ point with x := 1 }
.
The structure type can be specified if not inferable:
{ x := 1, y := 2 : Point }
.
Instances For
@x
disables automatic insertion of implicit parameters of the constant x
.
@e
for any term e
also disables the insertion of implicit lambdas at this position.
Instances For
.(e)
marks an "inaccessible pattern", which does not influence evaluation of the pattern match, but may be necessary for type-checking.
In contrast to regular patterns, e
may be an arbitrary term of the appropriate type.
Instances For
Instances For
Instances For
Implicit binder. In regular applications without @
, it is automatically inserted
and solved by unification whenever all explicit parameters before it are specified.
Instances For
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.
Instances For
Instance-implicit binder. In regular applications without @
, it is automatically inserted
and solved by typeclass inference of the specified class.
Instances For
A bracketedBinder
matches any kind of binder group that uses some kind of brackets:
- An explicit binder like
(x y : A)
- An implicit binder like
{x y : A}
- A strict implicit binder,
⦃y z : A⦄
or its ASCII alternative{{y z : A}}
- An instance binder
[A]
or[x : A]
(multiple variables are not allowed here)
Instances For
Instances For
Useful for syntax quotations. Note that generic patterns such as `(matchAltExpr| | ... => $rhs)
should also
work with other rhsParser
s (of arity 1).
Instances For
Instances For
matchDiscr
matches a "match discriminant", either h : tm
or tm
, used in match
as
match h1 : e1, e2, h3 : e3 with ...
.
Instances For
Pattern matching. match e, ... with | p, ... => f | ...
matches each given
term e
against each pattern p
of a match alternative. When all patterns
of an alternative match, the match
term evaluates to the value of the
corresponding right-hand side f
with the pattern variables bound to the
respective matched values.
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.
Instances For
Empty match/ex falso. nomatch e
is of arbitrary type α : Sort u
if
Lean can show that an empty set of patterns is exhaustive given e
's type,
e.g. because it has no constructors.
Instances For
A resolved name literal. Evaluates to the full name of the given constant if existent in the current context, or else fails.
Instances For
let
is used to declare a local definition. Example:
let x := 1
let y := x + 1
x + y
Since functions are first class citizens in Lean, you can use let
to declare
local functions too.
let double := fun x => 2*x
double (double 3)
For recursive definitions, you should use let rec
.
You can also perform pattern matching using let
. For example,
assume p
has type Nat × Nat
, then you can write
let (x, y) := p
x + y
Instances For
let_delayed x := v; b
is similar to let x := v; b
, but b
is elaborated before v
.
Instances For
let
-declaration that is only included in the elaborated term if variable is still there.
It is often used when building macros.
Instances For
attrKind
matches ("scoped" <|> "local")?
, used before an attribute like @[local simp]
.
Instances For
letRecDecl
matches the body of a let-rec declaration: a doc comment, attributes, and then
a let declaration without the let
keyword, such as /-- foo -/ @[simp] bar := 1
.
Instances For
letRecDecls
matches letRecDecl,+
, a comma-separated list of let-rec declarations (see letRecDecl
).
Instances For
A macro which evaluates to the name of the currently elaborating declaration.
Instances For
clear% x; e
elaborates x
after clearing the free variable x
from the local context.
If x
cannot be cleared (due to dependencies), it will keep x
without failing.
Instances For
Helper parser for marking match
-alternatives that should not trigger errors if unused.
We use them to implement macro_rules
and elab_rules
Instances For
The extended field notation e.f
is roughly short for T.f e
where T
is the type of e
.
More precisely,
- if
e
is of a function type,e.f
is translated toFunction.f (p := e)
wherep
is the first explicit parameter of function type - if
e
is of a named typeT ...
and there is a declarationT.f
(possibly fromexport
),e.f
is translated toT.f (p := e)
wherep
is the first explicit parameter of typeT ...
- 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.
Instances For
x.{u, ...}
explicitly specifies the universes u, ...
of the constant x
.
Instances For
x@e
matches the pattern e
and binds its value to the identifier x
.
Instances For
e |>.x
is a shorthand for (e).x
.
It is especially useful for avoiding parentheses with repeated applications.
Instances For
h ▸ e
is a macro built on top of Eq.rec
and Eq.symm
definitions.
Given h : a = b
and e : p a
, the term h ▸ e
has type p b
.
You can also view h ▸ e
as a "type casting" operation
where you change the type of e
by using h
.
See the Chapter "Quantifiers and Equality" in the manual
"Theorem Proving in Lean" for additional information.
Instances For
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.
Instances For
A shorthand for panic! "unreachable code has been reached"
.
Instances For
dbg_trace e; body
evaluates to body
and prints e
(which can be an
interpolated string literal) to stderr. It should only be used for debugging.