Auxiliary type used to represent syntax categories. We mainly use auxiliary definitions with this type to attach doc strings to syntax categories.
Instances For
command
is the syntax category for things that appear at the top level
of a lean file. For example, def foo := 1
is a command
, as is
namespace Foo
and end Foo
. Commands generally have an effect on the state of
adding something to the environment (like a new definition), as well as
commands like variable
which modify future commands within a scope.
Equations
Instances For
term
is the builtin syntax category for terms. A term denotes an expression
in lean's type theory, for example 2 + 2
is a term. The difference between
Term
and Expr
is that the former is a kind of syntax, while the latter is
the result of elaboration. For example by simp
is also a Term
, but it elaborates
to different Expr
s depending on the context.
Equations
Instances For
tactic
is the builtin syntax category for tactics. These appear after
by
in proofs, and they are programs that take in the proof context
(the hypotheses in scope plus the type of the term to synthesize) and construct
a term of the expected type. For example, simp
is a tactic, used in:
example : 2 + 2 = 4 := by simp
Equations
Instances For
structInstFieldDecl
is the syntax category for value declarations for fields in structure instance notation.
For example, the := 1
and | 0 => 0 | n + 1 => n
in { x := 1, f | 0 => 0 | n + 1 => n }
are in the structInstFieldDecl
class.
Equations
Instances For
level
is a builtin syntax category for universe levels.
This is the u
in Sort u
: it can contain max
and imax
, addition with
constants, and variables.
Equations
Instances For
attr
is a builtin syntax category for attributes.
Declarations can be annotated with attributes using the @[...]
notation.
Equations
Instances For
stx
is a builtin syntax category for syntax. This is the abbreviated
parser notation used inside syntax
and macro
declarations.
Equations
Instances For
prio
is a builtin syntax category for priorities.
Priorities are used in many different attributes.
Higher numbers denote higher priority, and for example typeclass search will
try high priority instances before low priority.
In addition to literals like 37
, you can also use low
, mid
, high
, as well as
add and subtract priorities.
Equations
Instances For
prec
is a builtin syntax category for precedences. A precedence is a value
that expresses how tightly a piece of syntax binds: for example 1 + 2 * 3
is
parsed as 1 + (2 * 3)
because *
has a higher precedence than +
.
Higher numbers denote higher precedence.
In addition to literals like 37
, there are some special named precedence levels:
arg
for the precedence of function argumentsmax
for the highest precedence used in term parsers (not actually the maximum possible value)lead
for the precedence of terms not supposed to be used as arguments and you can also add and subtract precedences.
Equations
Instances For
DSL for specifying parser precedences and priorities
Addition of precedences. This is normally used only for offsetting, e.g. max + 1
.
Equations
Instances For
Subtraction of precedences. This is normally used only for offsetting, e.g. max - 1
.
Equations
Instances For
Addition of priorities. This is normally used only for offsetting, e.g. default + 1
.
Equations
Instances For
Subtraction of priorities. This is normally used only for offsetting, e.g. default - 1
.
Equations
Instances For
Equations
Equations
Maximum precedence used in term parsers, in particular for terms in
function position (ident
, paren
, ...)
Equations
Instances For
Precedence used for application arguments (do
, by
, ...).
Equations
Instances For
Precedence used for terms not supposed to be used as arguments (let
, have
, ...).
Equations
Instances For
Parentheses are used for grouping precedence expressions.
Equations
Instances For
(min+1)
(we can only write min+1
after Meta.lean
)
Equations
Instances For
max:prec
as a term. It is equivalent to eval_prec max
for eval_prec
defined at Meta.lean
.
We use max_prec
to workaround bootstrapping issues.
Equations
Instances For
The default priority default = 1000
, which is used when no priority is set.
Equations
Instances For
The standardized "low" priority low = 100
, for things that should be lower than default priority.
Equations
Instances For
The standardized "medium" priority mid = 500
. This is lower than default
, and higher than low
.
Equations
Instances For
The standardized "high" priority high = 10000
, for things that should be higher than default priority.
Equations
Instances For
Parentheses are used for grouping priority expressions.
Equations
Instances For
p+
is shorthand for many1(p)
. It uses parser p
1 or more times, and produces a
nullNode
containing the array of parsed results. This parser has arity 1.
If p
has arity more than 1, it is auto-grouped in the items generated by the parser.
Equations
Instances For
p*
is shorthand for many(p)
. It uses parser p
0 or more times, and produces a
nullNode
containing the array of parsed results. This parser has arity 1.
If p
has arity more than 1, it is auto-grouped in the items generated by the parser.
Equations
Instances For
(p)?
is shorthand for optional(p)
. It uses parser p
0 or 1 times, and produces a
nullNode
containing the array of parsed results. This parser has arity 1.
p
is allowed to have arity n > 1 (in which case the node will have either 0 or n children),
but if it has arity 0 then the result will be ambiguous.
Because ?
is an identifier character, ident?
will not work as intended.
You have to write either ident ?
or (ident)?
for it to parse as the ?
combinator
applied to the ident
parser.
Equations
Instances For
p1 <|> p2
is shorthand for orelse(p1, p2)
, and parses either p1
or p2
.
It does not backtrack, meaning that if p1
consumes at least one token then
p2
will not be tried. Therefore, the parsers should all differ in their first
token. The atomic(p)
parser combinator can be used to locally backtrack a parser.
(For full backtracking, consider using extensible syntax classes instead.)
On success, if the inner parser does not generate exactly one node, it will be
automatically wrapped in a group
node, so the result will always be arity 1.
The <|>
combinator does not generate a node of its own, and in particular
does not tag the inner parsers to distinguish them, which can present a problem
when reconstructing the parse. A well formed <|>
parser should use disjoint
node kinds for p1
and p2
.
Equations
Instances For
p,*
is shorthand for sepBy(p, ",")
. It parses 0 or more occurrences of
p
separated by ,
, that is: empty | p | p,p | p,p,p | ...
.
It produces a nullNode
containing a SepArray
with the interleaved parser
results. It has arity 1, and auto-groups its component parser if needed.
Equations
Instances For
p,+
is shorthand for sepBy(p, ",")
. It parses 1 or more occurrences of
p
separated by ,
, that is: p | p,p | p,p,p | ...
.
It produces a nullNode
containing a SepArray
with the interleaved parser
results. It has arity 1, and auto-groups its component parser if needed.
Equations
Instances For
p,*,?
is shorthand for sepBy(p, ",", allowTrailingSep)
.
It parses 0 or more occurrences of p
separated by ,
, possibly including
a trailing ,
, that is: empty | p | p, | p,p | p,p, | p,p,p | ...
.
It produces a nullNode
containing a SepArray
with the interleaved parser
results. It has arity 1, and auto-groups its component parser if needed.
Equations
Instances For
p,+,?
is shorthand for sepBy1(p, ",", allowTrailingSep)
.
It parses 1 or more occurrences of p
separated by ,
, possibly including
a trailing ,
, that is: p | p, | p,p | p,p, | p,p,p | ...
.
It produces a nullNode
containing a SepArray
with the interleaved parser
results. It has arity 1, and auto-groups its component parser if needed.
Equations
Instances For
!p
parses the negation of p
. That is, it fails if p
succeeds, and
otherwise parses nothing. It has arity 0.
Equations
Instances For
The nat_lit n
macro constructs "raw numeric literals". This corresponds to the
Expr.lit (.natVal n)
constructor in the Expr
data type.
Normally, when you write a numeral like #check 37
, the parser turns this into
an application of OfNat.ofNat
to the raw literal 37
to cast it into the
target type, even if this type is Nat
(so the cast is the identity function).
But sometimes it is necessary to talk about the raw numeral directly,
especially when proving properties about the ofNat
function itself.
Equations
Instances For
Function composition, usually written with the infix operator ∘
. A new function is created from
two existing functions, where one function's output is used as input to the other.
Examples:
Function.comp List.reverse (List.drop 2) [3, 2, 4, 1] = [1, 4]
(List.reverse ∘ List.drop 2) [3, 2, 4, 1] = [1, 4]
Conventions for notations in identifiers:
- The recommended spelling of
∘
in identifiers iscomp
.
Equations
Instances For
The product type, usually written α × β
. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an α
and the second element is a
β
.
Products nest to the right, so (x, y, z) : α × β × γ
is equivalent to (x, (y, z)) : α × (β × γ)
.
Conventions for notations in identifiers:
- The recommended spelling of
×
in identifiers isProd
.
Equations
Instances For
A product type in which the types may be propositions, usually written α ×' β
.
This type is primarily used internally and as an implementation detail of proof automation. It is rarely useful in hand-written code.
Conventions for notations in identifiers:
- The recommended spelling of
×'
in identifiers isPProd
.
Equations
Instances For
Divisibility. a ∣ b
(typed as \|
) means that there is some c
such that b = a * c
.
Conventions for notations in identifiers:
- The recommended spelling of
∣
in identifiers isdvd
.
Equations
Instances For
a ||| b
computes the bitwise OR of a
and b
.
The meaning of this notation is type-dependent.
Conventions for notations in identifiers:
- The recommended spelling of
|||
in identifiers isor
.
Equations
Instances For
a ^^^ b
computes the bitwise XOR of a
and b
.
The meaning of this notation is type-dependent.
Conventions for notations in identifiers:
- The recommended spelling of
^^^
in identifiers isxor
.
Equations
Instances For
a &&& b
computes the bitwise AND of a
and b
.
The meaning of this notation is type-dependent.
Conventions for notations in identifiers:
- The recommended spelling of
&&&
in identifiers isand
.
Equations
Instances For
a + b
computes the sum of a
and b
.
The meaning of this notation is type-dependent.
Conventions for notations in identifiers:
- The recommended spelling of
+
in identifiers isadd
.
Equations
Instances For
a - b
computes the difference of a
and b
.
The meaning of this notation is type-dependent.
- For natural numbers, this operator saturates at 0:
a - b = 0
whena ≤ b
.
Conventions for notations in identifiers:
- The recommended spelling of
-
in identifiers issub
(when used as a binary operator).
Equations
Instances For
a * b
computes the product of a
and b
.
The meaning of this notation is type-dependent.
Conventions for notations in identifiers:
- The recommended spelling of
*
in identifiers ismul
.
Equations
Instances For
a / b
computes the result of dividing a
by b
.
The meaning of this notation is type-dependent.
- For most types like
Nat
,Int
,Rat
,Real
,a / 0
is defined to be0
. - For
Nat
,a / b
rounds downwards. - For
Int
,a / b
rounds downwards ifb
is positive or upwards ifb
is negative. It is implemented asInt.ediv
, the unique function satisfyinga % b + b * (a / b) = a
and0 ≤ a % b < natAbs b
forb ≠ 0
. Other rounding conventions are available using the functionsInt.fdiv
(floor rounding) andInt.tdiv
(truncation rounding). - For
Float
,a / 0
follows the IEEE 754 semantics for division, usually resulting ininf
ornan
.
Conventions for notations in identifiers:
- The recommended spelling of
/
in identifiers isdiv
.
Equations
Instances For
a % b
computes the remainder upon dividing a
by b
.
The meaning of this notation is type-dependent.
Conventions for notations in identifiers:
- The recommended spelling of
%
in identifiers ismod
.
Equations
Instances For
a <<< b
computes a
shifted to the left by b
places.
The meaning of this notation is type-dependent.
- On
Nat
, this is equivalent toa * 2 ^ b
. - On
UInt8
and other fixed width unsigned types, this is the same but truncated to the bit width.
Conventions for notations in identifiers:
- The recommended spelling of
<<<
in identifiers isshiftLeft
.
Equations
Instances For
a >>> b
computes a
shifted to the right by b
places.
The meaning of this notation is type-dependent.
Conventions for notations in identifiers:
- The recommended spelling of
>>>
in identifiers isshiftRight
.
Equations
Instances For
a ^ b
computes a
to the power of b
.
The meaning of this notation is type-dependent.
Conventions for notations in identifiers:
- The recommended spelling of
^
in identifiers ispow
.
Equations
Instances For
a ++ b
is the result of concatenation of a
and b
, usually read "append".
The meaning of this notation is type-dependent.
Conventions for notations in identifiers:
- The recommended spelling of
++
in identifiers isappend
.
Equations
Instances For
-a
computes the negative or opposite of a
.
The meaning of this notation is type-dependent.
Conventions for notations in identifiers:
- The recommended spelling of
-
in identifiers isneg
(when used as a unary operator).
Equations
Instances For
The implementation of ~~~a : α
.
Conventions for notations in identifiers:
- The recommended spelling of
~~~
in identifiers isnot
.
Equations
Instances For
a⁻¹
computes the inverse of a
.
The meaning of this notation is type-dependent.
Equations
Instances For
a • b
computes the product of a
and b
.
The meaning of this notation is type-dependent, but it is intended to be used for left actions.
Conventions for notations in identifiers:
- The recommended spelling of
•
in identifiers issmul
.
Equations
Instances For
Remark: the infix commands above ensure a delaborator is generated for each relations.
We redefine the macros below to be able to use the auxiliary binop%
elaboration helper for binary operators.
It addresses issue #382.
We have a macro to make x • y
notation participate in the expression tree elaborator,
like other arithmetic expressions such as +
, *
, /
, ^
, =
, inequalities, etc.
The macro is using the leftact%
elaborator introduced in
this RFC.
As a concrete example of the effect of this macro, consider
variable [Ring R] [AddCommMonoid M] [Module R M] (r : R) (N : Submodule R M) (m : M) (n : N)
#check m + r • n
Without the macro, the expression would elaborate as m + ↑(r • n : ↑N) : M
.
With the macro, the expression elaborates as m + r • (↑n : M) : M
.
To get the first interpretation, one can write m + (r • n :)
.
Here is a quick review of the expression tree elaborator:
- It builds up an expression tree of all the immediately accessible operations
that are marked with
binop%
,unop%
,leftact%
,rightact%
,binrel%
, etc. - It elaborates every leaf term of this tree
(without an expected type, so as if it were temporarily wrapped in
(... :)
). - Using the types of each elaborated leaf, it computes a supremum type they can all be coerced to, if such a supremum exists.
- It inserts coercions around leaf terms wherever needed.
The hypothesis is that individual expression trees tend to be calculations with respect to a single algebraic structure.
Note(kmill): If we were to remove HSMul
and switch to using SMul
directly,
then the expression tree elaborator would not be able to insert coercions within the right operand;
they would likely appear as ↑(x • y)
rather than x • ↑y
, unlike other arithmetic operations.
The less-equal relation: x ≤ y
Conventions for notations in identifiers:
- The recommended spelling of
<=
in identifiers isle
(prefer≤
over<=
).
Equations
Instances For
The less-equal relation: x ≤ y
Conventions for notations in identifiers:
- The recommended spelling of
≤
in identifiers isle
.
Equations
Instances For
The less-than relation: x < y
Conventions for notations in identifiers:
- The recommended spelling of
<
in identifiers islt
.
Equations
Instances For
a ≥ b
is an abbreviation for b ≤ a
.
Conventions for notations in identifiers:
- The recommended spelling of
>=
in identifiers isge
(prefer≥
over>=
).
Equations
Instances For
a ≥ b
is an abbreviation for b ≤ a
.
Conventions for notations in identifiers:
- The recommended spelling of
≥
in identifiers isge
.
Equations
Instances For
a > b
is an abbreviation for b < a
.
Conventions for notations in identifiers:
- The recommended spelling of
>
in identifiers isgt
.
Equations
Instances For
The equality relation. It has one introduction rule, Eq.refl
.
We use a = b
as notation for Eq a b
.
A fundamental property of equality is that it is an equivalence relation.
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)
example : a = d :=
Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given h1 : a = b
and h2 : p a
, we can construct a proof for p b
using substitution: Eq.subst h1 h2
.
Example:
example (α : Type) (a b : α) (p : α → Prop)
(h1 : a = b) (h2 : p a) : p b :=
Eq.subst h1 h2
example (α : Type) (a b : α) (p : α → Prop)
(h1 : a = b) (h2 : p a) : p b :=
h1 ▸ h2
The triangle in the second presentation is a macro built on top of Eq.subst
and Eq.symm
, and you can enter it by typing \t
.
For more information: Equality
Conventions for notations in identifiers:
- The recommended spelling of
=
in identifiers iseq
.
Equations
Instances For
Boolean equality, notated as a == b
.
Conventions for notations in identifiers:
- The recommended spelling of
==
in identifiers isbeq
.
Equations
Instances For
Heterogeneous equality. HEq a b
asserts that a
and b
have the same
type, and casting a
across the equality yields b
, and vice versa.
You should avoid using this type if you can. Heterogeneous equality does not
have all the same properties as Eq
, because the assumption that the types of
a
and b
are equal is often too weak to prove theorems of interest. One
important non-theorem is the analogue of congr
: If HEq f g
and HEq x y
and f x
and g y
are well typed it does not follow that HEq (f x) (g y)
.
(This does follow if you have f = g
instead.) However if a
and b
have
the same type then a = b
and HEq a b
are equivalent.
Equations
Instances For
Remark: the infix commands above ensure a delaborator is generated for each relations.
We redefine the macros below to be able to use the auxiliary binrel%
elaboration helper for binary relations.
It has better support for applying coercions. For example, suppose we have binrel% Eq n i
where n : Nat
and
i : Int
. The default elaborator fails because we don't have a coercion from Int
to Nat
, but
binrel%
succeeds because it also tries a coercion from Nat
to Int
even when the nat occurs before the int.
And a b
, or a ∧ b
, is the conjunction of propositions. It can be
constructed and destructed like a pair: if ha : a
and hb : b
then
⟨ha, hb⟩ : a ∧ b
, and if h : a ∧ b
then h.left : a
and h.right : b
.
Conventions for notations in identifiers:
- The recommended spelling of
/\
in identifiers isand
(prefer∧
over/\
).
Equations
Instances For
And a b
, or a ∧ b
, is the conjunction of propositions. It can be
constructed and destructed like a pair: if ha : a
and hb : b
then
⟨ha, hb⟩ : a ∧ b
, and if h : a ∧ b
then h.left : a
and h.right : b
.
Conventions for notations in identifiers:
- The recommended spelling of
∧
in identifiers isand
.
Equations
Instances For
Or a b
, or a ∨ b
, is the disjunction of propositions. There are two
constructors for Or
, called Or.inl : a → a ∨ b
and Or.inr : b → a ∨ b
,
and you can use match
or cases
to destruct an Or
assumption into the
two cases.
Conventions for notations in identifiers:
- The recommended spelling of
\/
in identifiers isor
(prefer∨
over\/
).
Equations
Instances For
Or a b
, or a ∨ b
, is the disjunction of propositions. There are two
constructors for Or
, called Or.inl : a → a ∨ b
and Or.inr : b → a ∨ b
,
and you can use match
or cases
to destruct an Or
assumption into the
two cases.
Conventions for notations in identifiers:
- The recommended spelling of
∨
in identifiers isor
.
Equations
Instances For
Not p
, or ¬p
, is the negation of p
. It is defined to be p → False
,
so if your goal is ¬p
you can use intro h
to turn the goal into
h : p ⊢ False
, and if you have hn : ¬p
and h : p
then hn h : False
and (hn h).elim
will prove anything.
For more information: Propositional Logic
Conventions for notations in identifiers:
- The recommended spelling of
¬
in identifiers isnot
.
Equations
Instances For
Boolean “and”, also known as conjunction. and x y
can be written x && y
.
The corresponding propositional connective is And : Prop → Prop → Prop
, written with the ∧
operator.
The Boolean and
is a @[macro_inline]
function in order to give it short-circuiting evaluation:
if x
is false
then y
is not evaluated at runtime.
Conventions for notations in identifiers:
- The recommended spelling of
&&
in identifiers isand
.
Equations
Instances For
Boolean “or”, also known as disjunction. or x y
can be written x || y
.
The corresponding propositional connective is Or : Prop → Prop → Prop
, written with the ∨
operator.
The Boolean or
is a @[macro_inline]
function in order to give it short-circuiting evaluation:
if x
is true
then y
is not evaluated at runtime.
Conventions for notations in identifiers:
- The recommended spelling of
||
in identifiers isor
.
Equations
Instances For
Boolean negation, also known as Boolean complement. not x
can be written !x
.
This is a function that maps the value true
to false
and the value false
to true
. The
propositional connective is Not : Prop → Prop
.
Conventions for notations in identifiers:
- The recommended spelling of
!
in identifiers isnot
.
Equations
Instances For
The membership relation a ∈ s : Prop
where a : α
, s : γ
.
Conventions for notations in identifiers:
- The recommended spelling of
∈
in identifiers ismem
.
Equations
Instances For
a ∉ b
is negated elementhood. It is notation for ¬ (a ∈ b)
.
Conventions for notations in identifiers:
- The recommended spelling of
∉
in identifiers isnot_mem
.
Equations
Instances For
The list whose first element is head
, where tail
is the rest of the list.
Usually written head :: tail
.
Conventions for notations in identifiers:
- The recommended spelling of
::
in identifiers iscons
.
Equations
Instances For
Applies a function inside a functor. This is used to overload the <$>
operator.
When mapping a constant function, use Functor.mapConst
instead, because it may be more
efficient.
Conventions for notations in identifiers:
- The recommended spelling of
<$>
in identifiers ismap
.
Equations
Instances For
Sequences two computations, allowing the second to depend on the value computed by the first.
If x : m α
and f : α → m β
, then x >>= f : m β
represents the result of executing x
to get
a value of type α
and then passing it to f
.
Conventions for notations in identifiers:
- The recommended spelling of
>>=
in identifiers isbind
.
Equations
Instances For
a <|> b
executes a
and returns the result, unless it fails in which
case it executes and returns b
. Because b
is not always executed, it
is passed as a thunk so it can be forced only when needed.
The meaning of this notation is type-dependent.
Conventions for notations in identifiers:
- The recommended spelling of
<|>
in identifiers isorElse
.
Equations
Instances For
a >> b
executes a
, ignores the result, and then executes b
.
If a
fails then b
is not executed. Because b
is not always executed, it
is passed as a thunk so it can be forced only when needed.
The meaning of this notation is type-dependent.
Conventions for notations in identifiers:
- The recommended spelling of
>>
in identifiers isandThen
.
Equations
Instances For
The implementation of the <*>
operator.
In a monad, mf <*> mx
is the same as do let f ← mf; x ← mx; pure (f x)
: it evaluates the
function first, then the argument, and applies one to the other.
To avoid surprising evaluation semantics, mx
is taken "lazily", using a Unit → f α
function.
Conventions for notations in identifiers:
- The recommended spelling of
<*>
in identifiers isseq
.
Equations
Instances For
Sequences the effects of two terms, discarding the value of the second. This function is usually
invoked via the <*
operator.
Given x : f α
and y : f β
, x <* y
runs x
, then runs y
, and finally returns the result of
x
.
The evaluation of the second argument is delayed by wrapping it in a function, enabling
“short-circuiting” behavior from f
.
Conventions for notations in identifiers:
- The recommended spelling of
<*
in identifiers isseqLeft
.
Equations
Instances For
Sequences the effects of two terms, discarding the value of the first. This function is usually
invoked via the *>
operator.
Given x : f α
and y : f β
, x *> y
runs x
, then runs y
, and finally returns the result of
y
.
The evaluation of the second argument is delayed by wrapping it in a function, enabling
“short-circuiting” behavior from f
.
Conventions for notations in identifiers:
- The recommended spelling of
*>
in identifiers isseqRight
.
Equations
Instances For
binderIdent
matches an ident
or a _
. It is used for identifiers in binding
position, where _
means that the value should be left unnamed and inaccessible.
Equations
Instances For
A case tag argument has the form tag x₁ ... xₙ
; it refers to tag tag
and renames
the last n
hypotheses to x₁ ... xₙ
.
Equations
Instances For
"Dependent" if-then-else, normally written via the notation if h : c then t(h) else e(h)
,
is sugar for dite c (fun h => t(h)) (fun h => e(h))
, and it is the same as
if c then t else e
except that t
is allowed to depend on a proof h : c
,
and e
can depend on h : ¬c
. (Both branches use the same name for the hypothesis,
even though it has different types in the two cases.)
We use this to be able to communicate the if-then-else condition to the branches.
For example, Array.get arr i h
expects a proof h : i < arr.size
in order to
avoid a bounds check, so you can write if h : i < arr.size then arr.get i h else ...
to avoid the bounds check inside the if branch. (Of course in this case we have only
lifted the check into an explicit if
, but we could also use this proof multiple times
or derive i < arr.size
from some other proposition that we are checking in the if
.)
Equations
Instances For
if c then t else e
is notation for ite c t e
, "if-then-else", which decides to
return t
or e
depending on whether c
is true or false. The explicit argument
c : Prop
does not have any actual computational content, but there is an additional
[Decidable c]
argument synthesized by typeclass inference which actually
determines how to evaluate c
to true or false. Write if h : c then t else e
instead for a "dependent if-then-else" dite
, which allows t
/e
to use the fact
that c
is true/false.
Equations
Instances For
if let pat := d then t else e
is a shorthand syntax for:
match d with
| pat => t
| _ => e
It matches d
against the pattern pat
and the bindings are available in t
.
If the pattern does not match, it returns e
instead.
Equations
Instances For
The conditional function.
cond c x y
is the same as if c then x else y
, but optimized for a Boolean condition rather than
a decidable proposition. It can also be written using the notation bif c then x else y
.
Just like ite
, cond
is declared @[macro_inline]
, which causes applications of cond
to be
unfolded. As a result, x
and y
are not evaluated at runtime until one of them is selected, and
only the selected branch is evaluated.
Equations
Instances For
Haskell-like pipe operator <|
. f <| x
means the same as the same as f x
,
except that it parses x
with lower precedence, which means that f <| g <| x
is interpreted as f (g x)
rather than (f g) x
.
Equations
Instances For
Haskell-like pipe operator |>
. x |> f
means the same as the same as f x
,
and it chains such that x |> f |> g
is interpreted as g (f x)
.
Equations
Instances For
Alternative syntax for <|
. f $ x
means the same as the same as f x
,
except that it parses x
with lower precedence, which means that f $ g $ x
is interpreted as f (g x)
rather than (f g) x
.
Equations
Instances For
All the elements of a type that satisfy a predicate.
Subtype p
, usually written { x : α // p x }
or { x // p x }
, contains all elements x : α
for
which p x
is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, { x : α // p x }
is represented identically to α
.
There is a coercion from { x : α // p x }
to α
, so elements of a subtype may be used where the
underlying type is expected.
Examples:
{ n : Nat // n % 2 = 0 }
is the type of even numbers.{ xs : Array String // xs.size = 5 }
is the type of arrays with fiveString
s.- Given
xs : List α
,List { x : α // x ∈ xs }
is the type of lists in which all elements are contained inxs
.
Conventions for notations in identifiers:
- The recommended spelling of
{ x // p x }
in identifiers issubtype
.
Equations
Instances For
without_expected_type t
instructs Lean to elaborate t
without an expected type.
Recall that terms such as match ... with ...
and ⟨...⟩
will postpone elaboration until
expected type is known. So, without_expected_type
is not effective in this case.
Equations
Instances For
- The
by_elab doSeq
expression runs thedoSeq
as aTermElabM Expr
to synthesize the expression. by_elab fun expectedType? => do doSeq
receives the expected type (anOption Expr
) as well.
Equations
Instances For
Category for carrying raw syntax trees between macros; any content is printed as is by the pretty printer. The only accepted parser for this category is an antiquotation.
Equations
Instances For
Equations
Normalize casts in an expression using the same method as the norm_cast
tactic.
Equations
Instances For
The attribute @[deprecated]
on a declaration indicates that the declaration
is discouraged for use in new code, and/or should be migrated away from in
existing code. It may be removed in a future version of the library.
@[deprecated myBetterDef]
means thatmyBetterDef
is the suggested replacement.@[deprecated myBetterDef "use myBetterDef instead"]
allows customizing the deprecation message.@[deprecated (since := "2024-04-21")]
records when the deprecation was first applied.
Equations
Instances For
The @[coe]
attribute on a function (which should also appear in a
instance : Coe A B := ⟨myFn⟩
declaration) allows the delaborator to show
applications of this function as ↑
when printing expressions.
Equations
Instances For
This attribute marks a code action, which is used to suggest new tactics or replace existing ones.
@[command_code_action kind]
: This is a code action which applies to applications of the commandkind
(a command syntax kind), which can replace the command or insert things before or after it.@[command_code_action kind₁ kind₂]
: shorthand for@[command_code_action kind₁, command_code_action kind₂]
.@[command_code_action]
: This is a command code action that applies to all commands. Use sparingly.
Equations
Instances For
When parent_dir
contains the current Lean file, include_str "path" / "to" / "file"
becomes
a string literal with the contents of the file at "parent_dir" / "path" / "to" / "file"
. If this
file cannot be read, elaboration fails.
Equations
Instances For
#reduce <expression>
reduces the expression <expression>
to its normal form. This
involves applying reduction rules until no further reduction is possible.
By default, proofs and types within the expression are not reduced. Use modifiers
(proofs := true)
and (types := true)
to reduce them.
Recall that propositions are types in Lean.
Warning: This can be a computationally expensive operation, especially for complex expressions.
Consider using #eval <expression>
for simple evaluation/execution
of expressions.
Equations
Instances For
A message filter specification for #guard_msgs
.
info
,warning
,error
: capture (non-trace) messages with the given severity level.trace
: captures trace messagesall
: capture all messages.
The filters can be prefixed with
check
(the default): capture and check the messagedrop
: drop the messagepass
: let the message pass through
If no filter is specified, check all
is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit pass all
at the end.
Equations
Instances For
Whitespace handling for #guard_msgs
:
whitespace := exact
requires an exact whitespace match.whitespace := normalized
converts all newline characters to a space before matching (the default). This allows breaking long lines.whitespace := lax
collapses whitespace to a single space before matching. In all cases, leading and trailing whitespace is trimmed before matching.
Equations
Instances For
Message ordering for #guard_msgs
:
ordering := exact
uses the exact ordering of the messages (the default).ordering := sorted
sorts the messages in lexicographic order. This helps with testing commands that are non-deterministic in their ordering.
Equations
Instances For
/-- ... -/ #guard_msgs in cmd
captures the messages generated by the command cmd
and checks that they match the contents of the docstring.
Basic example:
/--
error: unknown identifier 'x'
-/
#guard_msgs in
example : α := x
This checks that there is such an error and then consumes the message.
By default, the command captures all messages, but the filter condition can be adjusted. For example, we can select only warnings:
/--
warning: declaration uses 'sorry'
-/
#guard_msgs(warning) in
example : α := sorry
or only errors
#guard_msgs(error) in
example : α := sorry
In the previous example, since warnings are not captured there is a warning on sorry
.
We can drop the warning completely with
#guard_msgs(error, drop warning) in
example : α := sorry
In general, #guard_msgs
accepts a comma-separated list of configuration clauses in parentheses:
#guard_msgs (configElt,*) in cmd
By default, the configuration list is (check all, whitespace := normalized, ordering := exact)
.
Message filters select messages by severity:
info
,warning
,error
: (non-trace) messages with the given severity level.trace
: trace messagesall
: all messages.
The filters can be prefixed with the action to take:
check
(the default): capture and check the messagedrop
: drop the messagepass
: let the message pass through
If no filter is specified, check all
is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit pass all
at the end.
Whitespace handling (after trimming leading and trailing whitespace):
whitespace := exact
requires an exact whitespace match.whitespace := normalized
converts all newline characters to a space before matching (the default). This allows breaking long lines.whitespace := lax
collapses whitespace to a single space before matching.
Message ordering:
ordering := exact
uses the exact ordering of the messages (the default).ordering := sorted
sorts the messages in lexicographic order. This helps with testing commands that are non-deterministic in their ordering.
For example, #guard_msgs (error, drop all) in cmd
means to check warnings and drop
everything else.
The command elaborator has special support for #guard_msgs
for linting.
The #guard_msgs
itself wants to capture linter warnings,
so it elaborates the command it is attached to as if it were a top-level command.
However, the command elaborator runs linters for all top-level commands,
which would include #guard_msgs
itself, and would cause duplicate and/or uncaptured linter warnings.
The top-level command elaborator only runs the linters if #guard_msgs
is not present.
Equations
Instances For
Format and print the info trees for a given command. This is mostly useful for debugging info trees.
Equations
Instances For
Specify a premise selection engine. Note that Lean does not ship a default premise selection engine, so this is only useful in conjunction with a downstream package which provides one.
Equations
Instances For
#check_tactic t ~> r by commands
runs the tactic sequence commands
on a goal with t
and sees if the resulting expression has reduced it
to r
.
Equations
Instances For
#check_tactic_failure t by tac
runs the tactic tac
on a goal with t
and verifies it fails.
Equations
Instances For
#check_simp t ~> r
checks simp
reduces t
to r
.
Equations
Instances For
#check_simp t !~>
checks simp
fails on reducing t
.
Equations
Instances For
Time the elaboration of a command, and print the result (in milliseconds).
Example usage:
set_option maxRecDepth 100000 in
#time example : (List.range 500).length = 500 := rfl
Equations
Instances For
#discr_tree_key t
prints the discrimination tree keys for a term t
(or, if it is a single identifier, the type of that constant).
It uses the default configuration for generating keys.
For example,
#discr_tree_key (∀ {a n : Nat}, bar a (OfNat.ofNat n))
-- bar _ (@OfNat.ofNat Nat _ _)
#discr_tree_simp_key Nat.add_assoc
-- @HAdd.hAdd Nat Nat Nat _ (@HAdd.hAdd Nat Nat Nat _ _ _) _
#discr_tree_simp_key
is similar to #discr_tree_key
, but treats the underlying type
as one of a simp lemma, i.e. transforms it into an equality and produces the key of the
left-hand side.
Equations
Instances For
#discr_tree_key t
prints the discrimination tree keys for a term t
(or, if it is a single identifier, the type of that constant).
It uses the default configuration for generating keys.
For example,
#discr_tree_key (∀ {a n : Nat}, bar a (OfNat.ofNat n))
-- bar _ (@OfNat.ofNat Nat _ _)
#discr_tree_simp_key Nat.add_assoc
-- @HAdd.hAdd Nat Nat Nat _ (@HAdd.hAdd Nat Nat Nat _ _ _) _
#discr_tree_simp_key
is similar to #discr_tree_key
, but treats the underlying type
as one of a simp lemma, i.e. transforms it into an equality and produces the key of the
left-hand side.
Equations
Instances For
The seal foo
command ensures that the definition of foo
is sealed, meaning it is marked as [irreducible]
.
This command is particularly useful in contexts where you want to prevent the reduction of foo
in proofs.
In terms of functionality, seal foo
is equivalent to attribute [local irreducible] foo
.
This attribute specifies that foo
should be treated as irreducible only within the local scope,
which helps in maintaining the desired abstraction level without affecting global settings.
Equations
Instances For
The unseal foo
command ensures that the definition of foo
is unsealed, meaning it is marked as [semireducible]
, the
default reducibility setting. This command is useful when you need to allow some level of reduction of foo
in proofs.
Functionally, unseal foo
is equivalent to attribute [local semireducible] foo
.
Applying this attribute makes foo
semireducible only within the local scope.