Init.Prelude #
This is the first file in the Lean import hierarchy. It is responsible for setting
up basic definitions, most of which Lean already has "built in knowledge" about,
so it is important that they be set up in exactly this way. (For example, Lean will
use PUnit
in the desugaring of do
notation, or in the pattern match compiler.)
The identity function. id
takes an implicit argument α : Sort u
(a type in any universe), and an argument a : α
, and returns a
.
Although this may look like a useless function, one application of the identity
function is to explicitly put a type on an expression. If e
has type T
,
and T'
is definitionally equal to T
, then @id T' e
typechecks, and Lean
knows that this expression has type T'
rather than T
. This can make a
difference for typeclass inference, since T
and T'
may have different
typeclass instances on them. show T' from e
is sugar for an @id T' e
expression.
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
.
Instances For
The constant function that ignores its argument.
If a : α
, then Function.const β a : β → α
is the “constant function with value a
”. For all
arguments b : β
, Function.const β a b = a
.
Examples:
Function.const Bool 10 true = 10
Function.const Bool 10 false = 10
Function.const String 10 "any string" = 10
Equations
- Function.const β a x✝ = a
Instances For
The encoding of let_fun x := v; b
is letFun v (fun x => b)
.
This is equal to (fun x => b) v
, so the value of x
is not accessible to b
.
This is in contrast to let x := v; b
, where the value of x
is accessible to b
.
There is special support for letFun
.
Both WHNF and simp
are aware of letFun
and can reduce it when zeta reduction is enabled,
despite the fact it is marked irreducible
.
For metaprogramming, the function Lean.Expr.letFun?
can be used to recognize a let_fun
expression
to extract its parts as if it were a let
expression.
Instances For
inferInstance
synthesizes a value of any target type by typeclass
inference. This function has the same type signature as the identity
function, but the square brackets on the [i : α]
argument means that it will
attempt to construct this argument by typeclass inference. (This will fail if
α
is not a class
.) Example:
#check (inferInstance : Inhabited Nat) -- Inhabited Nat
def foo : Inhabited (Nat × Nat) :=
inferInstance
example : foo.default = (default, default) :=
rfl
Equations
Instances For
inferInstanceAs α
synthesizes a value of any target type by typeclass
inference. This is just like inferInstance
except that α
is given
explicitly instead of being inferred from the target type. It is especially
useful when the target type is some α'
which is definitionally equal to α
,
but the instance we are looking for is only registered for α
(because
typeclass search does not unfold most definitions, but definitional equality
does.) Example:
#check inferInstanceAs (Inhabited Nat) -- Inhabited Nat
Equations
- inferInstanceAs α = i
Instances For
The canonical type with one element. This element is written ()
.
Unit
has a number of uses:
- It can be used to model control flow that returns from a function call without providing other information.
- Monadic actions that return
Unit
have side effects without computing values. - In polymorphic types, it can be used to indicate that no data is to be stored in a particular field.
Instances For
Auxiliary unsafe constant used by the Compiler when erasing proofs from code.
It may look strange to have an axiom that says "every proposition is true",
since this is obviously unsound, but the unsafe
marker ensures that the
kernel will not let this through into regular proofs. The lower levels of the
code generator don't need proofs in terms, so this is used to stub the proofs
out.
Auxiliary unsafe constant used by the Compiler to mark unreachable code.
Like lcProof
, this is an unsafe axiom
, which means that even though it is
not sound, the kernel will not let us use it for regular proofs.
Executing this expression to actually synthesize a value of type α
causes
immediate undefined behavior, and the compiler does take advantage of this
to optimize the code assuming that it is not called. If it is not optimized out,
it is likely to appear as a print message saying "unreachable code", but this
behavior is not guaranteed or stable in any way.
True
is a proposition and has only an introduction rule, True.intro : True
.
In other words, True
is simply true, and has a canonical proof, True.intro
For more information: Propositional Logic
- intro : True
True
is true, andTrue.intro
(or more commonly,trivial
) is the proof.
Instances For
False
is the empty proposition. Thus, it has no introduction rules.
It represents a contradiction. False
elimination rule, False.rec
,
expresses the fact that anything follows from a contradiction.
This rule is sometimes called ex falso (short for ex falso sequitur quodlibet),
or the principle of explosion.
For more information: Propositional Logic
Instances For
The empty type. It has no constructors.
Use Empty.elim
in contexts where a value of type Empty
is in scope.
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
.
Instances For
False.elim : False → C
says that from False
, any desired proposition
C
holds. Also known as ex falso quodlibet (EFQ) or the principle of explosion.
The target type is actually C : Sort u
which means it works for both
propositions and types. When executed, this acts like an "unreachable"
instruction: it is undefined behavior to run, but it will probably print
"unreachable code". (You would need to construct a proof of false to run it
anyway, which you can only do using sorry
or unsound axioms.)
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
.
Instances For
rfl : a = a
is the unique constructor of the equality type. This is the
same as Eq.refl
except that it takes a
implicitly instead of explicitly.
This is a more powerful theorem than it may appear at first, because although
the statement of the theorem is a = a
, Lean will allow anything that is
definitionally equal to that type. So, for instance, 2 + 2 = 4
is proven in
Lean by rfl
, because both sides are the same up to definitional equality.
Equations
- ⋯ = ⋯
Instances For
The substitution principle for equality. If a = b
and P a
holds,
then P b
also holds. We conventionally use the name motive
for P
here,
so that you can specify it explicitly using e.g.
Eq.subst (motive := fun x => x < 5)
if it is not otherwise inferred correctly.
This theorem is the underlying mechanism behind the rw
tactic, which is
essentially a fancy algorithm for finding good motive
arguments to usefully
apply this theorem to replace occurrences of a
with b
in the goal or
hypotheses.
For more information: Equality
Cast across a type equality. If h : α = β
is an equality of types, and
a : α
, then a : β
will usually not typecheck directly, but this function
will allow you to work around this and embed a
in type β
as cast h a : β
.
It is best to avoid this function if you can, because it is more complicated to reason about terms containing casts, but if the types don't match up definitionally sometimes there isn't anything better you can do.
For more information: Equality
Instances For
Congruence in the function argument: if a₁ = a₂
then f a₁ = f a₂
for
any (nondependent) function f
. This is more powerful than it might look at first, because
you can also use a lambda expression for f
to prove that
<something containing a₁> = <something containing a₂>
. This function is used
internally by tactics like congr
and simp
to apply equalities inside
subterms.
For more information: Equality
Congruence in both function and argument. If f₁ = f₂
and a₁ = a₂
then
f₁ a₁ = f₂ a₂
. This only works for nondependent functions; the theorem
statement is more complex in the dependent case.
For more information: Equality
Initialize the Quotient Module, which effectively adds the following definitions:
opaque Quot {α : Sort u} (r : α → α → Prop) : Sort u
opaque Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r
opaque Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
(∀ a b : α, r a b → Eq (f a) (f b)) → Quot r → β
opaque Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
(∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β q
Low-level quotient types. Quotient types coarsen the propositional equality for a type α
, so that
terms related by some relation r
are considered equal in Quot r
.
Set-theoretically, Quot r
can seen as the set of equivalence classes of α
modulo r
. Functions
from Quot r
must prove that they respect r
: to define a function f : Quot r → β
, it is
necessary to provide f' : α → β
and prove that for all x : α
and y : α
, r x y → f' x = f' y
.
Quot
is a built-in primitive:
Quot.mk
places elements of the underlying typeα
into the quotient.Quot.lift
allows the definition of functions from the quotient to some other type.Quot.sound
asserts the equality of elements related byr
.Quot.ind
is used to write proofs about quotients by assuming that all elements are constructed withQuot.mk
.
The relation r
is not required to be an equivalence relation; the resulting quotient type's
equality extends r
to an equivalence as a consequence of the rules for equality and quotients.
When r
is an equivalence relation, it can be more convenient to use the higher-level type
Quotient
.
Places an element of a type into the quotient that equates terms according to the provided relation.
Given v : α
and relation r : α → α → Prop
, Quot.mk r v : Quot r
is like v
, except all
observations of v
's value must respect r
.
Quot.mk
is a built-in primitive:
Quot
is the built-in quotient type.Quot.lift
allows the definition of functions from the quotient to some other type.Quot.sound
asserts the equality of elements related byr
.Quot.ind
is used to write proofs about quotients by assuming that all elements are constructed withQuot.mk
.
A reasoning principle for quotients that allows proofs about quotients to assume that all values are
constructed with Quot.mk
.
Quot.rec
is analogous to the recursor for a structure, and can
be used when the resulting type is not necessarily a proposition.
Quot.ind
is a built-in primitive:
Quot
is the built-in quotient type.Quot.mk
places elements of the underlying typeα
into the quotient.Quot.lift
allows the definition of functions from the quotient to some other type.Quot.sound
asserts the equality of elements related byr
.
Lifts a function from an underlying type to a function on a quotient, requiring that it respects the quotient's relation.
Given a relation r : α → α → Prop
and a quotient Quot r
, applying a function f : α → β
requires a proof a
that f
respects r
. In this case, Quot.lift f a : Quot r → β
computes the
same values as f
.
Lean's type theory includes a definitional reduction from
Quot.lift f h (Quot.mk r v)
to f v
.
Quot.lift
is a built-in primitive:
Quot
is the built-in quotient type.Quot.mk
places elements of the underlying typeα
into the quotient.Quot.sound
asserts the equality of elements related byr
Quot.ind
is used to write proofs about quotients by assuming that all elements are constructed withQuot.mk
; it is analogous to the recursor for a structure.
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.
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
.
- fst : α
The first element of a pair.
- snd : β
The second element of a pair.
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
.
- fst : α
The first element of a pair.
- snd : β
The second element of a pair.
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
.The recommended spelling of
/\
in identifiers isand
(prefer∧
over/\
).
- intro :: (
- left : a
Extract the left conjunct from a conjunction.
h : a ∧ b
thenh.left
, also notated ash.1
, is a proof ofa
. - right : b
Extract the right conjunct from a conjunction.
h : a ∧ b
thenh.right
, also notated ash.2
, is a proof ofb
. - )
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
.The recommended spelling of
\/
in identifiers isor
(prefer∨
over\/
).
Instances For
The Boolean values, true
and false
.
Logically speaking, this is equivalent to Prop
(the type of propositions). The distinction is
important for programming: both propositions and their proofs are erased in the code generator,
while Bool
corresponds to the Boolean type in most programming languages and carries precisely one
bit of run-time information.
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
.
- val : α
The value in the underlying type that satisfies the predicate.
- property : p self.val
The proof that
val
satisfies the predicatep
.
Instances For
Gadget for marking output parameters in type classes.
For example, the Membership
class is defined as:
class Membership (α : outParam (Type u)) (γ : Type v)
This means that whenever a typeclass goal of the form Membership ?α ?γ
comes
up, Lean will wait to solve it until ?γ
is known, but then it will run
typeclass inference, and take the first solution it finds, for any value of ?α
,
which thereby determines what ?α
should be.
This expresses that in a term like a ∈ s
, s
might be a Set α
or
List α
or some other type with a membership operation, and in each case
the "member" type α
is determined by looking at the container type.
Instances For
Gadget for marking semi output parameters in type classes.
Semi-output parameters influence the order in which arguments to type class
instances are processed. Lean determines an order where all non-(semi-)output
parameters to the instance argument have to be figured out before attempting to
synthesize an argument (that is, they do not contain assignable metavariables
created during TC synthesis). This rules out instances such as [Mul β] : Add α
(because β
could be anything). Marking a parameter as semi-output is a
promise that instances of the type class will always fill in a value for that
parameter.
For example, the Coe
class is defined as:
class Coe (α : semiOutParam (Sort u)) (β : Sort v)
This means that all Coe
instances should provide a concrete value for α
(i.e., not an assignable metavariable). An instance like Coe Nat Int
or Coe α (Option α)
is fine, but Coe α Nat
is not since it does not provide a value
for α
.
Equations
- semiOutParam α = α
Instances For
Auxiliary declaration used to implement named patterns like x@h:p
.
Equations
- a = a
Instances For
Auxiliary axiom used to implement the sorry
term and tactic.
The sorry
term/tactic expands to sorryAx _ (synthetic := false)
.
It 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 check if a declaration depends on sorry
either directly or indirectly by looking for sorryAx
in the output
of the #print axioms my_thm
command.
The synthetic
flag is false when a sorry
is written explicitly by the user, but it is
set to true
when a tactic fails to prove a goal, or if there is a type error
in the expression. A synthetic sorry
acts like a regular one, except that it
suppresses follow-up errors in order to prevent an error from causing a cascade
of other errors because the desired term was not constructed.
Inhabited α
is a typeclass that says that α
has a designated element,
called (default : α)
. This is sometimes referred to as a "pointed type".
This class is used by functions that need to return a value of the type
when called "out of domain". For example, Array.get! arr i : α
returns
a value of type α
when arr : Array α
, but if i
is not in range of
the array, it reports a panic message, but this does not halt the program,
so it must still return a value of type α
(and in fact this is required
for logical consistency), so in this case it returns default
.
- default : α
Instances
Nonempty α
is a typeclass that says that α
is not an empty type,
that is, there exists an element in the type. It differs from Inhabited α
in that Nonempty α
is a Prop
, which means that it does not actually carry
an element of α
, only a proof that there exists such an element.
Given Nonempty α
, you can construct an element of α
nonconstructively
using Classical.choice
.
Instances
The axiom of choice. Nonempty α
is a proof that α
has an element,
but the element itself is erased. The axiom choice
supplies a particular
element of α
given only this proof.
The textbook axiom of choice normally makes a family of choices all at once,
but that is implied from this formulation, because if α : ι → Type
is a
family of types and h : ∀ i, Nonempty (α i)
is a proof that they are all
nonempty, then fun i => Classical.choice (h i) : ∀ i, α i
is a family of
chosen elements. This is actually a bit stronger than the ZFC choice axiom;
this is sometimes called "global choice".
In Lean, we use the axiom of choice to derive the law of excluded middle
(see Classical.em
), so it will often show up in axiom listings where you
may not expect. You can use #print axioms my_thm
to find out if a given
theorem depends on this or other axioms.
This axiom can be used to construct "data", but obviously there is no algorithm
to compute it, so Lean will require you to mark any definition that would
involve executing Classical.choice
or other axioms as noncomputable
, and
will not produce any executable code for such definitions.
The elimination principle for Nonempty α
. If Nonempty α
, and we can
prove p
given any element x : α
, then p
holds. Note that it is essential
that p
is a Prop
here; the version with p
being a Sort u
is equivalent
to Classical.choice
.
A variation on Classical.choice
that uses typeclass inference to
infer the proof of Nonempty α
.
Equations
Instances For
Equations
- instInhabitedSort = { default := PUnit }
Equations
- instInhabitedForall α = { default := fun (x : α) => default }
Equations
- Pi.instInhabited = { default := fun (x : α) => default }
Lifts a proposition or type to a higher universe level.
PLift α
wraps a proof or value of type α
. The resulting type is in the next largest universe
after that of α
. In particular, propositions become data.
The related type ULift
can be used to lift a non-proposition type by any number of levels.
Examples:
(False : Prop)
(PLift False : Type)
([.up (by trivial), .up (by simp), .up (by decide)] : List (PLift True))
(Nat : Type 0)
(PLift Nat : Type 1)
- up :: (
- down : α
Extracts a wrapped proof or value from a universe-lifted proposition or type.
- )
Instances For
NonemptyType.{u}
is the type of nonempty types in universe u
.
It is mainly used in constant declarations where we wish to introduce a type
and simultaneously assert that it is nonempty, but otherwise make the type
opaque.
Instances For
NonemptyType
is inhabited, because PUnit
is a nonempty type.
Equations
- instInhabitedNonemptyType = { default := ⟨PUnit, ⋯⟩ }
Lifts a type to a higher universe level.
ULift α
wraps a value of type α
. Instead of occupying the same universe as α
, which would be
the minimal level, it takes a further level parameter and occupies their minimum. The resulting type
may occupy any universe that's at least as large as that of α
.
The resulting universe of the lifting operator is the first parameter, and may be written explicitly
while allowing α
's level to be inferred.
The related type PLift
can be used to lift a proposition or type by one level.
Examples:
(Nat : Type 0)
(ULift Nat : Type 0)
(ULift Nat : Type 1)
(ULift Nat : Type 5)
(ULift.{7} (PUnit : Type 3) : Type 7)
- up :: (
- down : α
Extracts a wrapped value from a universe-lifted type.
- )
Instances For
Bijection between α
and ULift.{v} α
Either a proof that p
is true or a proof that p
is false. This is equivalent to a Bool
paired
with a proof that the Bool
is true
if and only if p
is true.
Decidable
instances are primarily used via if
-expressions and the tactic decide
. In
conditional expressions, the Decidable
instance for the proposition is used to select a branch. At
run time, this case distinction code is identical to that which would be generated for a
Bool
-based conditional. In proofs, the tactic decide
synthesizes an instance of Decidable p
,
attempts to reduce it to isTrue h
, and then succeeds with the proof h
if it can.
Because Decidable
carries data, when writing @[simp]
lemmas which include a Decidable
instance
on the LHS, it is best to use {_ : Decidable p}
rather than [Decidable p]
so that non-canonical
instances can be found via unification rather than instance synthesis.
- isFalse
{p : Prop}
(h : ¬p)
: Decidable p
Proves that
p
is decidable by supplying a proof of¬p
- isTrue
{p : Prop}
(h : p)
: Decidable p
Proves that
p
is decidable by supplying a proof ofp
Instances
A decidable predicate.
A predicate is decidable if the corresponding proposition is Decidable
for each possible argument.
Equations
- DecidablePred r = ((a : α) → Decidable (r a))
Instances For
A decidable relation.
A relation is decidable if the corresponding proposition is Decidable
for all possible arguments.
Equations
- DecidableRel r = ((a : α) → (b : β) → Decidable (r a b))
Instances For
Propositional equality is Decidable
for all elements of a type.
In other words, an instance of DecidableEq α
is a means of deciding the proposition a = b
is
for all a b : α
.
Equations
- DecidableEq α = ((a b : α) → Decidable (a = b))
Instances For
Checks whether two terms of a type are equal using the type's DecidableEq
instance.
Instances For
Decides whether two Booleans are equal.
This function should normally be called via the DecidableEq Bool
instance that it exists to
support.
Equations
Instances For
Equations
BEq α
is a typeclass for supplying a boolean-valued equality relation on
α
, notated as a == b
. Unlike DecidableEq α
(which uses a = b
), this
is Bool
valued instead of Prop
valued, and it also does not have any
axioms like being reflexive or agreeing with =
. It is mainly intended for
programming applications. See LawfulBEq
for a version that requires that
==
and =
coincide.
Typically we prefer to put the "more variable" term on the left, and the "more constant" term on the right.
- beq : α → α → Bool
Boolean equality, notated as
a == b
.Conventions for notations in identifiers:
- The recommended spelling of
==
in identifiers isbeq
.
- The recommended spelling of
Instances
Equations
- instBEqOfDecidableEq = { beq := fun (a b : α) => decide (a = b) }
"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
- dite c t e = Decidable.casesOn h e t
Instances For
if-then-else #
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.
Instances For
Equations
Equations
Equations
Boolean operators #
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.
Instances For
The dependent conditional function, in which each branch is provided with a local assumption about the condition's value. This allows the value to be used in proofs as well as for control flow.
dcond c (fun h => x) (fun h => y)
is the same as if h : c then x else y
, but optimized for a
Boolean condition rather than a decidable proposition. Unlike the non-dependent version cond
,
there is no special notation for dcond
.
Just like ite
, dite
, and cond
, dcond
is declared @[macro_inline]
, which causes
applications of dcond
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. dcond
is intended for
metaprogramming use, rather than for use in verified programs, so behavioral lemmas are not
provided.
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.
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
.The recommended spelling of
||
in identifiers isor
.
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
.
Instances For
The natural numbers, starting at zero.
This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
GMP); at runtime, Nat
values that are sufficiently small are unboxed.
- zero : Nat
Zero, the smallest natural number.
Using
Nat.zero
explicitly should usually be avoided in favor of the literal0
, which is the simp normal form. - succ
(n : Nat)
: Nat
The successor of a natural number
n
.Using
Nat.succ n
should usually be avoided in favor ofn + 1
, which is the simp normal form.
Instances For
The class OfNat α n
powers the numeric literal parser. If you write
37 : α
, Lean will attempt to synthesize OfNat α 37
, and will generate
the term (OfNat.ofNat 37 : α)
.
There is a bit of infinite regress here since the desugaring apparently
still contains a literal 37
in it. The type of expressions contains a
primitive constructor for "raw natural number literals", which you can directly
access using the macro nat_lit 37
. Raw number literals are always of type Nat
.
So it would be more correct to say that Lean looks for an instance of
OfNat α (nat_lit 37)
, and it generates the term (OfNat.ofNat (nat_lit 37) : α)
.
- ofNat : α
The
OfNat.ofNat
function is automatically inserted by the parser when the user writes a numeric literal like1 : α
. Implementations of this typeclass can therefore customize the behavior ofn : α
based onn
andα
.
Instances
Equations
- instOfNatNat n = { ofNat := n }
Transitive chaining of proofs, used e.g. by calc
.
It takes two relations r
and s
as "input", and produces an "output"
relation t
, with the property that r a b
and s b c
implies t a c
.
The calc
tactic uses this so that when it sees a chain with a ≤ b
and b < c
it knows that this should be a proof of a < c
because there is an instance
Trans (·≤·) (·<·) (·<·)
.
- trans {a : α} {b : β} {c : γ} : r a b → s b c → t a c
Compose two proofs by transitivity, generalized over the relations involved.
Instances
The notation typeclass for heterogeneous addition.
This enables the notation a + b : γ
where a : α
, b : β
.
- hAdd : α → β → γ
a + b
computes the sum ofa
andb
. The meaning of this notation is type-dependent.Conventions for notations in identifiers:
- The recommended spelling of
+
in identifiers isadd
.
- The recommended spelling of
Instances
The notation typeclass for heterogeneous subtraction.
This enables the notation a - b : γ
where a : α
, b : β
.
- hSub : α → β → γ
a - b
computes the difference ofa
andb
. 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).
- For natural numbers, this operator saturates at 0:
Instances
The notation typeclass for heterogeneous multiplication.
This enables the notation a * b : γ
where a : α
, b : β
.
- hMul : α → β → γ
a * b
computes the product ofa
andb
. The meaning of this notation is type-dependent.Conventions for notations in identifiers:
- The recommended spelling of
*
in identifiers ismul
.
- The recommended spelling of
Instances
The notation typeclass for heterogeneous division.
This enables the notation a / b : γ
where a : α
, b : β
.
- hDiv : α → β → γ
a / b
computes the result of dividinga
byb
. 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
.
- For most types like
Instances
The notation typeclass for heterogeneous modulo / remainder.
This enables the notation a % b : γ
where a : α
, b : β
.
- hMod : α → β → γ
Instances
The notation typeclass for heterogeneous exponentiation.
This enables the notation a ^ b : γ
where a : α
, b : β
.
- hPow : α → β → γ
a ^ b
computesa
to the power ofb
. The meaning of this notation is type-dependent.Conventions for notations in identifiers:
- The recommended spelling of
^
in identifiers ispow
.
- The recommended spelling of
Instances
The notation typeclass for heterogeneous append.
This enables the notation a ++ b : γ
where a : α
, b : β
.
- hAppend : α → β → γ
a ++ b
is the result of concatenation ofa
andb
, usually read "append". The meaning of this notation is type-dependent.Conventions for notations in identifiers:
- The recommended spelling of
++
in identifiers isappend
.
- The recommended spelling of
Instances
The typeclass behind the notation a <|> b : γ
where a : α
, b : β
.
Because b
is "lazy" in this notation, it is passed as Unit → β
to the
implementation so it can decide when to evaluate it.
- hOrElse : α → (Unit → β) → γ
a <|> b
executesa
and returns the result, unless it fails in which case it executes and returnsb
. Becauseb
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
.
- The recommended spelling of
Instances
The typeclass behind the notation a >> b : γ
where a : α
, b : β
.
Because b
is "lazy" in this notation, it is passed as Unit → β
to the
implementation so it can decide when to evaluate it.
- hAndThen : α → (Unit → β) → γ
a >> b
executesa
, ignores the result, and then executesb
. Ifa
fails thenb
is not executed. Becauseb
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
.
- The recommended spelling of
Instances
The typeclass behind the notation a &&& b : γ
where a : α
, b : β
.
- hAnd : α → β → γ
a &&& b
computes the bitwise AND ofa
andb
. The meaning of this notation is type-dependent.Conventions for notations in identifiers:
- The recommended spelling of
&&&
in identifiers isand
.
- The recommended spelling of
Instances
The typeclass behind the notation a ^^^ b : γ
where a : α
, b : β
.
- hXor : α → β → γ
a ^^^ b
computes the bitwise XOR ofa
andb
. The meaning of this notation is type-dependent.Conventions for notations in identifiers:
- The recommended spelling of
^^^
in identifiers isxor
.
- The recommended spelling of
Instances
The typeclass behind the notation a ||| b : γ
where a : α
, b : β
.
- hOr : α → β → γ
a ||| b
computes the bitwise OR ofa
andb
. The meaning of this notation is type-dependent.Conventions for notations in identifiers:
- The recommended spelling of
|||
in identifiers isor
.
- The recommended spelling of
Instances
The typeclass behind the notation a <<< b : γ
where a : α
, b : β
.
- hShiftLeft : α → β → γ
a <<< b
computesa
shifted to the left byb
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
.
- On
Instances
The typeclass behind the notation a >>> b : γ
where a : α
, b : β
.
- hShiftRight : α → β → γ
a >>> b
computesa
shifted to the right byb
places. The meaning of this notation is type-dependent.Conventions for notations in identifiers:
- The recommended spelling of
>>>
in identifiers isshiftRight
.
- The recommended spelling of
Instances
The notation typeclass for negation.
This enables the notation -a : α
where a : α
.
- neg : α → α
-a
computes the negative or opposite ofa
. 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).
- The recommended spelling of
Instances
The homogeneous version of HPow
: a ^ b : α
where a : α
, b : β
.
(The right argument is not the same as the left since we often want this even
in the homogeneous case.)
Types can choose to subscribe to particular defaulting behavior by providing
an instance to either NatPow
or HomogeneousPow
:
NatPow
is for types whose exponents is preferentially aNat
.HomogeneousPow
is for types whose base and exponent are preferentially the same.
- pow : α → β → α
a ^ b
computesa
to the power ofb
. SeeHPow
.
Instances
The homogeneous version of Pow
where the exponent is a Nat
.
The purpose of this class is that it provides a default Pow
instance,
which can be used to specialize the exponent to Nat
during elaboration.
For example, if x ^ 2
should preferentially elaborate with 2 : Nat
then x
's type should
provide an instance for this class.
- pow : α → Nat → α
Instances
The completely homogeneous version of Pow
where the exponent has the same type as the base.
The purpose of this class is that it provides a default Pow
instance,
which can be used to specialize the exponent to have the same type as the base's type during elaboration.
This is to say, a type should provide an instance for this class in case x ^ y
should be elaborated
with both x
and y
having the same type.
For example, the Float
type provides an instance of this class, which causes expressions
such as (2.2 ^ 2.2 : Float)
to elaborate.
- pow : α → α → α
a ^ b
computesa
to the power ofb
wherea
andb
both have the same type.
Instances
The typeclass behind the notation ~~~a : α
where a : α
.
- complement : α → α
The implementation of
~~~a : α
.Conventions for notations in identifiers:
- The recommended spelling of
~~~
in identifiers isnot
.
- The recommended spelling of
Instances
The homogeneous version of HShiftLeft
: a <<< b : α
where a b : α
.
- shiftLeft : α → α → α
The implementation of
a <<< b : α
. SeeHShiftLeft
.
Instances
The homogeneous version of HShiftRight
: a >>> b : α
where a b : α
.
- shiftRight : α → α → α
The implementation of
a >>> b : α
. SeeHShiftRight
.
Instances
Equations
- instPowNat = { pow := fun (a : α) (n : Nat) => NatPow.pow a n }
Equations
- instPowOfHomogeneousPow = { pow := fun (a b : α) => HomogeneousPow.pow a b }
Equations
- instHAppendOfAppend = { hAppend := fun (a b : α) => Append.append a b }
Equations
- instHOrElseOfOrElse = { hOrElse := fun (a : α) (b : Unit → α) => OrElse.orElse a b }
Equations
- instHAndThenOfAndThen = { hAndThen := fun (a : α) (b : Unit → α) => AndThen.andThen a b }
Equations
- instHAndOfAndOp = { hAnd := fun (a b : α) => AndOp.and a b }
Equations
- instHXorOfXor = { hXor := fun (a b : α) => Xor.xor a b }
Equations
- instHOrOfOrOp = { hOr := fun (a b : α) => OrOp.or a b }
Equations
- instHShiftLeftOfShiftLeft = { hShiftLeft := fun (a b : α) => ShiftLeft.shiftLeft a b }
Equations
- instHShiftRightOfShiftRight = { hShiftRight := fun (a b : α) => ShiftRight.shiftRight a b }
The typeclass behind the notation a ∈ s : Prop
where a : α
, s : γ
.
Because α
is an outParam
, the "container type" γ
determines the type
of the elements of the container.
- mem : γ → α → Prop
The membership relation
a ∈ s : Prop
wherea : α
,s : γ
.Conventions for notations in identifiers:
- The recommended spelling of
∈
in identifiers ismem
.
- The recommended spelling of
Instances
Addition of natural numbers, typically used via the +
operator.
This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.
Instances For
Multiplication of natural numbers, usually accessed via the *
operator.
This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.
Instances For
The power operation on natural numbers, usually accessed via the ^
operator.
This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.
Instances For
Boolean equality of natural numbers, usually accessed via the ==
operator.
This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.
Equations
Instances For
A decision procedure for equality of natural numbers, usually accessed via the DecidableEq Nat
instance.
This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.
Examples:
Instances For
The Boolean less-than-or-equal-to comparison on natural numbers.
This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.
Examples:
Equations
Instances For
The predecessor of a natural number is one less than it. The precedessor of 0
is defined to be
0
.
This definition is overridden in the compiler with an efficient implementation. This definition is the logical model.
Instances For
A decision procedure for non-strict inequality of natural numbers, usually accessed via the
DecidableLE Nat
instance.
Examples:
A decision procedure for strict inequality of natural numbers, usually accessed via the
DecidableLT Nat
instance.
Examples:
(if 3 < 4 then "yes" else "no") = "yes"
(if 4 < 4 then "yes" else "no") = "no"
(if 6 < 4 then "yes" else "no") = "no"
show 5 < 12 by decide
Subtraction of natural numbers, truncated at 0
. Usually used via the -
operator.
If a result would be less than zero, then the result is zero.
This definition is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.
Examples:
5 - 3 = 2
8 - 2 = 6
8 - 8 = 0
8 - 20 = 0
Instances For
Gets the word size of the curent platform. The word size may be 64 or 32 bits.
This function is opaque because there is no guarantee at compile time that the target will have the same word size as the host. It also helps avoid having type checking be architecture-dependent.
Lean only works on 64 and 32 bit systems. This fact is visible in the return type.
The word size of the current platform, which may be 64 or 32 bits.
Equations
Instances For
Natural numbers less than some upper bound.
In particular, a Fin n
is a natural number i
with the constraint that i < n
. It is the
canonical type with n
elements.
Instances For
A bitvector of the specified width.
This is represented as the underlying Nat
number in both the runtime
and the kernel, inheriting all the special support for Nat
.
- ofFin :: (
Interpret a bitvector as a number less than
2^w
. O(1), because we useFin
as the internal representation of a bitvector.- )
Instances For
Equations
Equations
- instDecidableLtBitVec x y = inferInstanceAs (Decidable (x.toNat < y.toNat))
Equations
- instDecidableLeBitVec x y = inferInstanceAs (Decidable (x.toNat ≤ y.toNat))
The number of distinct values representable by UInt8
, that is, 2^8 = 256
.
Equations
- UInt8.size = 256
Instances For
Converts a natural number to an 8-bit unsigned integer. Requires a proof that the number is small
enough to be representable without overflow; it must be smaller than 2^8
.
This function is overridden at runtime with an efficient implementation.
Equations
- UInt8.ofNatLT n h = { toBitVec := n#'h }
Instances For
Decides whether two 8-bit unsigned integers are equal. Usually accessed via the DecidableEq UInt8
instance.
This function is overridden at runtime with an efficient implementation.
Examples:
UInt8.decEq 123 123 = .isTrue rfl
(if (6 : UInt8) = 7 then "yes" else "no") = "no"
show (7 : UInt8) = 7 by decide
Instances For
Equations
- instInhabitedUInt8 = { default := UInt8.ofNatLT 0 instInhabitedUInt8.proof_1 }
The number of distinct values representable by UInt16
, that is, 2^16 = 65536
.
Equations
- UInt16.size = 65536
Instances For
Converts a natural number to a 16-bit unsigned integer. Requires a proof that the number is small
enough to be representable without overflow; it must be smaller than 2^16
.
This function is overridden at runtime with an efficient implementation.
Equations
- UInt16.ofNatLT n h = { toBitVec := n#'h }
Instances For
Decides whether two 16-bit unsigned integers are equal. Usually accessed via the
DecidableEq UInt16
instance.
This function is overridden at runtime with an efficient implementation.
Examples:
UInt16.decEq 123 123 = .isTrue rfl
(if (6 : UInt16) = 7 then "yes" else "no") = "no"
show (7 : UInt16) = 7 by decide
Instances For
Equations
Equations
- instInhabitedUInt16 = { default := UInt16.ofNatLT 0 instInhabitedUInt16.proof_1 }
The number of distinct values representable by UInt32
, that is, 2^32 = 4294967296
.
Equations
- UInt32.size = 4294967296
Instances For
Converts a natural number to a 32-bit unsigned integer. Requires a proof that the number is small
enough to be representable without overflow; it must be smaller than 2^32
.
This function is overridden at runtime with an efficient implementation.
Equations
- UInt32.ofNatLT n h = { toBitVec := n#'h }
Instances For
Decides whether two 32-bit unsigned integers are equal. Usually accessed via the
DecidableEq UInt32
instance.
This function is overridden at runtime with an efficient implementation.
Examples:
UInt32.decEq 123 123 = .isTrue rfl
(if (6 : UInt32) = 7 then "yes" else "no") = "no"
show (7 : UInt32) = 7 by decide
Instances For
Equations
Equations
- instInhabitedUInt32 = { default := UInt32.ofNatLT 0 instInhabitedUInt32.proof_1 }
Decides whether one 8-bit unsigned integer is strictly less than another. Usually accessed via the
DecidableLT UInt32
instance.
This function is overridden at runtime with an efficient implementation.
Examples:
(if (6 : UInt32) < 7 then "yes" else "no") = "yes"
(if (5 : UInt32) < 5 then "yes" else "no") = "no"
show ¬((7 : UInt32) < 7) by decide
Instances For
Decides whether one 32-bit signed integer is less than or equal to another. Usually accessed via the
DecidableLE UInt32
instance.
This function is overridden at runtime with an efficient implementation.
Examples:
(if (15 : UInt32) ≤ 15 then "yes" else "no") = "yes"
(if (15 : UInt32) ≤ 5 then "yes" else "no") = "no"
(if (5 : UInt32) ≤ 15 then "yes" else "no") = "yes"
show (7 : UInt32) ≤ 7 by decide
Instances For
Equations
- instDecidableLtUInt32 a b = a.decLt b
Equations
- instDecidableLeUInt32 a b = a.decLe b
The number of distinct values representable by UInt64
, that is, 2^64 = 18446744073709551616
.
Equations
- UInt64.size = 18446744073709551616
Instances For
Converts a natural number to a 64-bit unsigned integer. Requires a proof that the number is small
enough to be representable without overflow; it must be smaller than 2^64
.
This function is overridden at runtime with an efficient implementation.
Equations
- UInt64.ofNatLT n h = { toBitVec := n#'h }
Instances For
Decides whether two 64-bit unsigned integers are equal. Usually accessed via the
DecidableEq UInt64
instance.
This function is overridden at runtime with an efficient implementation.
Examples:
UInt64.decEq 123 123 = .isTrue rfl
(if (6 : UInt64) = 7 then "yes" else "no") = "no"
show (7 : UInt64) = 7 by decide
Instances For
Equations
Equations
- instInhabitedUInt64 = { default := UInt64.ofNatLT 0 instInhabitedUInt64.proof_1 }
Unsigned integers that are the size of a word on the platform's architecture.
On a 32-bit architecture, USize
is equivalent to UInt32
. On a 64-bit machine, it is equivalent
to UInt64
.
- ofBitVec :: (
- toBitVec : BitVec System.Platform.numBits
Unpacks a
USize
into aBitVec System.Platform.numBits
. This function is overridden with a native implementation. - )
Instances For
Converts a natural number to a USize
. Requires a proof that the number is small enough to be
representable without overflow.
This function is overridden at runtime with an efficient implementation.
Equations
- USize.ofNatLT n h = { toBitVec := n#'h }
Instances For
Decides whether two word-sized unsigned integers are equal. Usually accessed via the
DecidableEq USize
instance.
This function is overridden at runtime with an efficient implementation.
Examples:
USize.decEq 123 123 = .isTrue rfl
(if (6 : USize) = 7 then "yes" else "no") = "no"
show (7 : USize) = 7 by decide
Instances For
Equations
- instInhabitedUSize = { default := USize.ofNatLT 0 USize.size_pos }
A UInt32
denotes a valid Unicode code point if it is less than 0x110000
and it is also not a
surrogate code point (the range 0xd800
to 0xdfff
inclusive).
Equations
- n.isValidChar = n.toNat.isValidChar
Instances For
Characters are Unicode scalar values.
- val : UInt32
The underlying Unicode scalar value as a
UInt32
. - valid : self.val.isValidChar
The value must be a legal scalar value.
Instances For
Pack a Nat
encoding a valid codepoint into a Char
.
This function is overridden with a native implementation.
Equations
- Char.ofNatAux n h = { val := { toBitVec := n#'⋯ }, valid := h }
Instances For
Converts a Nat
into a Char
. If the Nat
does not encode a valid Unicode scalar value, '\0'
is
returned instead.
Equations
- Char.ofNat n = if h : n.isValidChar then Char.ofNatAux n h else { val := { toBitVec := 0#'Char.ofNat.proof_1 }, valid := Char.ofNat.proof_2 }
Instances For
Returns the number of bytes required to encode this Char
in UTF-8.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- instInhabitedOption = { default := none }
Apply a function to an optional value, if present.
From the perspective of Option
as a container with at most one value, this is analogous to
List.map
. It can also be accessed via the Functor Option
instance.
Examples:
Equations
- Option.map f (some x) = some (f x)
- Option.map f none = none
Instances For
Linked lists: ordered lists, in which each element has a reference to the next element.
Most operations on linked lists take time proportional to the length of the list, because each element must be traversed to find the next element.
List α
is isomorphic to Array α
, but they are useful for different things:
List α
is easier for reasoning, andArray α
is modeled as a wrapper aroundList α
.List α
works well as a persistent data structure, when many copies of the tail are shared. When the value is not shared,Array α
will have better performance because it can do destructive updates.
- nil
{α : Type u}
: List α
The empty list, usually written
[]
.Conventions for notations in identifiers:
- The recommended spelling of
[]
in identifiers isnil
.
- The recommended spelling of
- cons
{α : Type u}
(head : α)
(tail : List α)
: List α
The list whose first element is
head
, wheretail
is the rest of the list. Usually writtenhead :: tail
.Conventions for notations in identifiers:
The recommended spelling of
::
in identifiers iscons
.The recommended spelling of
[a]
in identifiers issingleton
.
Instances For
Equations
- instInhabitedList = { default := [] }
Equations
The length of a list.
This function is overridden in the compiler to lengthTR
, which uses constant stack space.
Examples:
Instances For
Auxiliary function for List.lengthTR
.
Equations
- [].lengthTRAux x✝ = x✝
- (head :: as).lengthTRAux x✝ = as.lengthTRAux x✝.succ
Instances For
The length of a list.
This is a tail-recursive version of List.length
, used to implement List.length
without running
out of stack space.
Examples:
Equations
- as.lengthTR = as.lengthTRAux 0
Instances For
Returns the element at the provided index, counting from 0
.
In other words, for i : Fin as.length
, as.get i
returns the i
'th element of the list as
.
Because the index is a Fin
bounded by the list's length, the index will never be out of bounds.
Examples:
["spring", "summer", "fall", "winter"].get (2 : Fin 4) = "fall"
["spring", "summer", "fall", "winter"].get (0 : Fin 4) = "spring"
Instances For
Replaces the value at (zero-based) index n
in l
with a
. If the index is out of bounds, then
the list is returned unmodified.
Examples:
["water", "coffee", "soda", "juice"].set 1 "tea" = ["water", "tea", "soda", "juice"]
["water", "coffee", "soda", "juice"].set 4 "tea" = ["water", "coffee", "soda", "juice"]
Equations
Instances For
Folds a function over a list from the left, accumulating a value starting with init
. The
accumulated value is combined with the each element of the list in order, using f
.
Examples:
[a, b, c].foldl f z = f (f (f z a) b) c
[1, 2, 3].foldl (· ++ toString ·) "" = "123"
[1, 2, 3].foldl (s!"({·} {·})") "" = "((( 1) 2) 3)"
Equations
- List.foldl f x✝ [] = x✝
- List.foldl f x✝ (b :: l) = List.foldl f (f x✝ b) l
Instances For
Adds an element to the end of a list.
The added element is the last element of the resulting list.
Examples:
List.concat ["red", "yellow"] "green" = ["red", "yellow", "green"]
List.concat [1, 2, 3] 4 = [1, 2, 3, 4]
List.concat [] () = [()]
Instances For
A string is a sequence of Unicode code points.
At runtime, strings are represented by dynamic arrays
of bytes using the UTF-8 encoding. Both the size in bytes (String.utf8ByteSize
) and in characters
(String.length
) are cached and take constant time. Many operations on strings perform in-place
modifications when the reference to the string is unique.
Instances For
Decides whether two strings are equal. Normally used via the DecidableEq String
instance and the
=
operator.
At runtime, this function is overridden with an efficient native implementation.
Instances For
Equations
A byte position in a String
, according to its UTF-8 encoding.
Character positions (counting the Unicode code points rather than bytes) are represented by plain
Nat
s. Indexing a String
by a String.Pos
takes constant time, while character positions need to
be translated internally to byte positions, which takes linear time.
A byte position p
is valid for a string s
if 0 ≤ p ≤ s.endPos
and p
lies on a UTF-8
character boundary.
- byteIdx : Nat
Get the underlying byte index of a
String.Pos
Instances For
A region or slice of some underlying string.
A substring contains an string together with the start and end byte positions of a region of interest. Actually extracting a substring requires copying and memory allocation, while many substrings of the same underlying string may exist with very little overhead, and they are more convenient than tracking the bounds by hand.
Using its constructor explicitly, it is possible to construct a Substring
in which one or both of
the positions is invalid for the string. Many operations will return unexpected or confusing results
if the start and stop positions are not valid. Instead, it's better to use API functions that ensure
the validity of the positions in a substring to create and manipulate them.
- str : String
The underlying string.
- startPos : String.Pos
The byte position of the start of the string slice.
- stopPos : String.Pos
The byte position of the end of the string slice.
Instances For
Equations
- instInhabitedSubstring = { default := { str := "", startPos := { }, stopPos := { } } }
The number of bytes used by the string's UTF-8 encoding.
At runtime, this function takes constant time because the byte length of strings is cached.
Equations
- { data := s }.utf8ByteSize = String.utf8ByteSize.go s
Instances For
Equations
- String.utf8ByteSize.go [] = 0
- String.utf8ByteSize.go (c :: cs) = String.utf8ByteSize.go cs + c.utf8Size
Instances For
Equations
- instHAddPos = { hAdd := fun (p₁ p₂ : String.Pos) => { byteIdx := p₁.byteIdx + p₂.byteIdx } }
Equations
- instHSubPos = { hSub := fun (p₁ p₂ : String.Pos) => { byteIdx := p₁.byteIdx - p₂.byteIdx } }
Equations
- instHAddPosChar = { hAdd := fun (p : String.Pos) (c : Char) => { byteIdx := p.byteIdx + c.utf8Size } }
Equations
- instHAddPosString = { hAdd := fun (p : String.Pos) (s : String) => { byteIdx := p.byteIdx + s.utf8ByteSize } }
Equations
- instDecidableLePos p₁ p₂ = inferInstanceAs (Decidable (p₁.byteIdx ≤ p₂.byteIdx))
Equations
- instDecidableLtPos p₁ p₂ = inferInstanceAs (Decidable (p₁.byteIdx < p₂.byteIdx))
A UTF-8 byte position that points at the end of a string, just after the last character.
Equations
- s.endPos = { byteIdx := s.utf8ByteSize }
Instances For
Converts a String
into a Substring
that denotes the entire string.
Equations
- s.toSubstring = { str := s, startPos := { }, stopPos := s.endPos }
Instances For
Converts a String
into a Substring
that denotes the entire string.
This is a version of String.toSubstring
that doesn't have an @[inline]
annotation.
Equations
- s.toSubstring' = s.toSubstring
Instances For
This function will cast a value of type α
to type β
, and is a no-op in the
compiler. This function is extremely dangerous because there is no guarantee
that types α
and β
have the same data representation, and this can lead to
memory unsafety. It is also logically unsound, since you could just cast
True
to False
. For all those reasons this function is marked as unsafe
.
It is implemented by lifting both α
and β
into a common universe, and then
using cast (lcProof : ULift (PLift α) = ULift (PLift β))
to actually perform
the cast. All these operations are no-ops in the compiler.
Using this function correctly requires some knowledge of the data representation of the source and target types. Some general classes of casts which are safe in the current runtime:
Array α
toArray β
whereα
andβ
have compatible representations, or more generally for other inductive types.Quot α r
andα
.@Subtype α p
andα
, or generally any structure containing only one non-Prop
field of typeα
.- Casting
α
to/fromNonScalar
whenα
is a boxed generic type (i.e. a function that accepts an arbitrary typeα
and is not specialized to a scalar type likeUInt8
).
Equations
- unsafeCast a = (cast ⋯ { down := { down := a } }).down.down
Instances For
(panic "msg" : α)
has a built-in implementation which prints msg
to
the error buffer. It does not terminate execution, and because it is a safe
function, it still has to return an element of α
, so it takes [Inhabited α]
and returns default
. It is primarily intended for debugging in pure contexts,
and assertion failures.
Because this is a pure function with side effects, it is marked as
@[never_extract]
so that the compiler will not perform common sub-expression
elimination and other optimizations that assume that the expression is pure.
Instances For
Array α
is the type of dynamic arrays with elements
from α
. This type has special support in the runtime.
Arrays perform best when unshared. As long as there is never more than one reference to an array, all updates will be performed destructively. This results in performance comparable to mutable arrays in imperative programming languages.
An array has a size and a capacity. The size is the number of elements present in the array, while
the capacity is the amount of memory currently allocated for elements. The size is accessible via
Array.size
, but the capacity is not observable from Lean code. Array.emptyWithCapacity n
creates
an array which is equal to #[]
, but internally allocates an array of capacity n
. When the size
exceeds the capacity, allocation is required to grow the array.
From the point of view of proofs, Array α
is just a wrapper around List α
.
- toList : List α
Converts an
Array α
into aList α
that contains the same elements in the same order.At runtime, this is implemented by
Array.toListImpl
and isO(n)
in the length of the array.
Instances For
Converts a List α
into an Array α
.
O(|xs|)
. At runtime, this operation is implemented by List.toArrayImpl
and takes time linear in
the length of the list. List.toArray
should be used instead of Array.mk
.
Examples:
[1, 2, 3].toArray = #[1, 2, 3]
["monday", "wednesday", friday"].toArray = #["monday", "wednesday", friday"].
Instances For
Constructs a new empty array with initial capacity c
.
This will be deprecated in favor of Array.emptyWithCapacity
in the future.
Equations
- Array.mkEmpty c = { toList := [] }
Instances For
Constructs a new empty array with initial capacity c
.
Equations
- Array.emptyWithCapacity c = { toList := [] }
Instances For
Constructs a new empty array with initial capacity 0
.
Use Array.emptyWithCapacity
to create an array with a greater initial capacity.
Equations
Instances For
Gets the number of elements stored in an array.
This is a cached value, so it is O(1)
to access. The space allocated for an array, referred to as
its capacity, is at least as large as its size, but may be larger. The capacity of an array is an
internal detail that's not observable by Lean code.
Instances For
Use the indexing notation a[i]
instead.
Access an element from an array without needing a runtime bounds checks,
using a Nat
index and a proof that it is in bounds.
This function does not use get_elem_tactic
to automatically find the proof that
the index is in bounds. This is because the tactic itself needs to look up values in
arrays.
Equations
- a.getInternal i h = a.toList.get ⟨i, h⟩
Instances For
Returns the element at the provided index, counting from 0
. Returns the fallback value v₀
if the
index is out of bounds.
To return an Option
depending on whether the index is in bounds, use a[i]?
. To panic if the
index is out of bounds, use a[i]!
.
Examples:
#["spring", "summer", "fall", "winter"].getD 2 "never" = "fall"
#["spring", "summer", "fall", "winter"].getD 0 "never" = "spring"
#["spring", "summer", "fall", "winter"].getD 4 "never" = "never"
Equations
- a.getD i v₀ = if h : i < a.size then a.getInternal i h else v₀
Instances For
Use the indexing notation a[i]!
instead.
Access an element from an array, or panic if the index is out of bounds.
Equations
- a.get!Internal i = a.getD i default
Instances For
Adds an element to the end of an array. The resulting array's size is one greater than the input array. If there are no other references to the array, then it is modified in-place.
This takes amortized O(1)
time because Array α
is represented by a dynamic array.
Examples:
Instances For
Create array #[]
Equations
Instances For
Slower Array.append
used in quotations.
Equations
- as.appendCore bs = Array.appendCore.loop bs bs.size 0 as
Instances For
Equations
- Array.appendCore.loop bs i j as = if hlt : j < bs.size then match i with | 0 => as | i'.succ => Array.appendCore.loop bs i' (j + 1) (as.push (bs.getInternal j hlt)) else as
Instances For
Returns the slice of as
from indices start
to stop
(exclusive). The resulting array has size
(min stop as.size) - start
.
If start
is greater or equal to stop
, the result is empty. If stop
is greater than the size of
as
, the size is used instead.
Examples:
#[0, 1, 2, 3, 4].extract 1 3 = #[1, 2]
#[0, 1, 2, 3, 4].extract 1 30 = #[1, 2, 3, 4]
#[0, 1, 2, 3, 4].extract 0 0 = #[]
#[0, 1, 2, 3, 4].extract 2 1 = #[]
#[0, 1, 2, 3, 4].extract 2 2 = #[]
#[0, 1, 2, 3, 4].extract 2 3 = #[2]
#[0, 1, 2, 3, 4].extract 2 4 = #[2, 3]
Equations
- as.extract start stop = Array.extract.loop as ((min stop as.size).sub start) start (Array.emptyWithCapacity ((min stop as.size).sub start))
Instances For
Equations
- Array.extract.loop as i j bs = if hlt : j < as.size then match i with | 0 => bs | i'.succ => Array.extract.loop as i' (j + 1) (bs.push (as.getInternal j hlt)) else bs
Instances For
The >>=
operator is overloaded via instances of bind
.
Bind
is typically used via Monad
, which extends it.
- bind {α β : Type u} : m α → (α → m β) → m β
Sequences two computations, allowing the second to depend on the value computed by the first.
If
x : m α
andf : α → m β
, thenx >>= f : m β
represents the result of executingx
to get a value of typeα
and then passing it tof
.Conventions for notations in identifiers:
- The recommended spelling of
>>=
in identifiers isbind
.
- The recommended spelling of
Instances
A functor in the sense used in functional programming, which means a function f : Type u → Type v
has a way of mapping a function over its contents. This map
operator is written <$>
, and
overloaded via Functor
instances.
This map
function should respect identity and function composition. In other words, for all terms
v : f α
, it should be the case that:
id <$> v = v
For all functions
h : β → γ
andg : α → β
,(h ∘ g) <$> v = h <$> g <$> v
While all Functor
instances should live up to these requirements, they are not required to prove
that they do. Proofs may be required or provided via the LawfulFunctor
class.
Assuming that instances are lawful, this definition corresponds to the category-theoretic notion of functor in the special case where the category is the category of types and functions between them.
- map {α β : Type u} : (α → β) → f α → f β
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
.
- The recommended spelling of
- mapConst {α β : Type u} : α → f β → f α
Mapping a constant function.
Given
a : α
andv : f α
,mapConst a v
is equivalent toFunction.const _ a <$> v
. For some functors, this can be implemented more efficiently; for all other functors, the default implementation may be used.
Instances
The <*>
operator is overloaded using the function Seq.seq
.
While <$>
from the class Functor
allows an ordinary function to be mapped over its contents,
<*>
allows a function that's “inside” the functor to be applied. When thinking about f
as
possible side effects, this captures evaluation order: seq
arranges for the effects that produce
the function to occur prior to those that produce the argument value.
For most applications, Applicative
or Monad
should be used rather than Seq
itself.
The implementation of the
<*>
operator.In a monad,
mf <*> mx
is the same asdo 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 aUnit → f α
function.Conventions for notations in identifiers:
- The recommended spelling of
<*>
in identifiers isseq
.
- The recommended spelling of
Instances
The <*
operator is overloaded using seqLeft
.
When thinking about f
as potential side effects, <*
evaluates first the left and then the right
argument for their side effects, discarding the value of the right argument and returning the value
of the left argument.
For most applications, Applicative
or Monad
should be used rather than SeqLeft
itself.
Sequences the effects of two terms, discarding the value of the second. This function is usually invoked via the
<*
operator.Given
x : f α
andy : f β
,x <* y
runsx
, then runsy
, and finally returns the result ofx
.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
.
- The recommended spelling of
Instances
The *>
operator is overloaded using seqRight
.
When thinking about f
as potential side effects, *>
evaluates first the left and then the right
argument for their side effects, discarding the value of the left argument and returning the value
of the right argument.
For most applications, Applicative
or Monad
should be used rather than SeqLeft
itself.
Sequences the effects of two terms, discarding the value of the first. This function is usually invoked via the
*>
operator.Given
x : f α
andy : f β
,x *> y
runsx
, then runsy
, and finally returns the result ofy
.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
.
- The recommended spelling of
Instances
An applicative functor is more powerful than a Functor
, but
less powerful than a Monad
.
Applicative functors capture sequencing of effects with the <*>
operator, overloaded as seq
, but
not data-dependent effects. The results of earlier computations cannot be used to control later
effects.
Applicative functors should satisfy four laws. Instances of Applicative
are not required to prove
that they satisfy these laws, which are part of the LawfulApplicative
class.
Instances
Monads are an abstraction of sequential control flow and side effects used in functional programming. Monads allow both sequencing of effects and data-dependent effects: the values that result from an early step may influence the effects carried out in a later step.
The Monad
API may be used directly. However, it is most commonly accessed through
do
-notation.
Most Monad
instances provide implementations of pure
and bind
, and use default implementations
for the other methods inherited from Applicative
. Monads should satisfy certain laws, but
instances are not required to prove this. An instance of LawfulMonad
expresses that a given
monad's operations are lawful.
Instances
Equations
- instInhabitedForallOfMonad = { default := pure }
Computations in the monad m
can be run in the monad n
. These translations are inserted
automatically by the compiler.
Usually, n
consists of some number of monad transformers applied to m
, but this is not
mandatory.
New instances should use this class, MonadLift
. Clients that require one monad to be liftable into
another should instead request MonadLiftT
, which is the reflexive, transitive closure of
MonadLift
.
- monadLift {α : Type u} : m α → n α
Translates an action from monad
m
into monadn
.
Instances
Computations in the monad m
can be run in the monad n
. These translations are inserted
automatically by the compiler.
Usually, n
consists of some number of monad transformers applied to m
, but this is not
mandatory.
This is the reflexive, transitive closure of MonadLift
. Clients that require one monad to be
liftable into another should request an instance of MonadLiftT
. New instances should instead be
defined for MonadLift
itself.
- monadLift {α : Type u} : m α → n α
Translates an action from monad
m
into monadn
.
Instances
Equations
- instMonadLiftTOfMonadLift m n o = { monadLift := fun {α : Type ?u.30} (x : m α) => MonadLift.monadLift (monadLift x) }
Equations
- instMonadLiftT m = { monadLift := fun {α : Type ?u.10} (x : m α) => x }
Typeclass used for adapting monads. This is similar to MonadLift
, but instances are allowed to
make use of default state for the purpose of synthesizing such an instance, if necessary.
Every MonadLift
instance gives a MonadEval
instance.
The purpose of this class is for the #eval
command,
which looks for a MonadEval m CommandElabM
or MonadEval m IO
instance.
- monadEval {α : Type u} : m α → n α
Evaluates a value from monad
m
into monadn
.
Instances
Equations
- instMonadEvalOfMonadLift = { monadEval := fun {α : Type ?u.19} => MonadLift.monadLift }
Equations
- instMonadEvalTOfMonadEval m n o = { monadEval := fun {α : Type ?u.30} (x : m α) => MonadEval.monadEval (MonadEvalT.monadEval x) }
Equations
- instMonadEvalT m = { monadEval := fun {α : Type ?u.10} (x : m α) => x }
A way to interpret a fully-polymorphic function in m
into n
. Such a function can be thought of
as one that may change the effects in m
, but can't do so based on specific values that are
provided.
Clients of MonadFunctor
should typically use MonadFunctorT
, which is the reflexive, transitive
closure of MonadFunctor
. New instances should be defined for MonadFunctor.
Lifts a fully-polymorphic transformation of
m
inton
.
Instances
A way to interpret a fully-polymorphic function in m
into n
. Such a function can be thought of
as one that may change the effects in m
, but can't do so based on specific values that are
provided.
This is the reflexive, transitive closure of MonadFunctor
. It automatically chains together
MonadFunctor
instances as needed. Clients of MonadFunctor
should typically use MonadFunctorT
,
but new instances should be defined for MonadFunctor
.
Lifts a fully-polymorphic transformation of
m
inton
.
Instances
Equations
- One or more equations did not get rendered due to their size.
Equations
- monadFunctorRefl m = { monadMap := fun {α : Type ?u.12} (f : {β : Type ?u.12} → m β → m β) => f }
Except ε α
is a type which represents either an error of type ε
or a successful result with a
value of type α
.
Except ε : Type u → Type v
is a Monad
that represents computations that may throw exceptions:
the pure
operation is Except.ok
and the bind
operation returns the first encountered
Except.error
.
- error
{ε : Type u}
{α : Type v}
: ε → Except ε α
A failure value of type
ε
- ok
{ε : Type u}
{α : Type v}
: α → Except ε α
A success value of type
α
Instances For
Equations
- instInhabitedExcept = { default := Except.error default }
Exception monads provide the ability to throw errors and handle errors.
In this class, ε
is a semiOutParam
, which means that it can influence the choice of instance.
MonadExcept ε
provides the same operations, but requires that ε
be inferrable from m
.
tryCatchThe
, which takes an explicit exception type, is used to desugar try ... catch ...
steps
inside do
-blocks when the handlers have type annotations.
- throw {α : Type v} : ε → m α
Throws an exception of type
ε
to the nearest enclosingcatch
. Catches errors thrown in
body
, passing them tohandler
. Errors inhandler
are not caught.
Instances
Throws an exception, with the exception type specified explicitly. This is useful when a monad supports throwing more than one type of exception.
Use throw
for a version that expects the exception type to be inferred from m
.
Equations
- throwThe ε e = MonadExceptOf.throw e
Instances For
Catches errors, recovering using handle
. The exception type is specified explicitly. This is useful when a monad
supports throwing or handling more than one type of exception.
Use tryCatch
, for a version that expects the exception type to be inferred from m
.
Equations
- tryCatchThe ε x handle = MonadExceptOf.tryCatch x handle
Instances For
Exception monads provide the ability to throw errors and handle errors.
In this class, ε
is an outParam
, which means that it is inferred from m
. MonadExceptOf ε
provides the same operations, but allows ε
to influence instance synthesis.
MonadExcept.tryCatch
is used to desugar try ... catch ...
steps inside do
-blocks when the
handlers do not have exception type annotations.
- throw {α : Type v} : ε → m α
Throws an exception of type
ε
to the nearest enclosing handler. Catches errors thrown in
body
, passing them tohandler
. Errors inhandler
are not caught.
Instances
Re-interprets an Except ε
action in an exception monad m
, succeeding if it succeeds and throwing
an exception if it throws an exception.
Instances For
Equations
- instMonadExceptOfMonadExceptOf ε m = { throw := fun {α : Type ?u.18} => throwThe ε, tryCatch := fun {α : Type ?u.18} => tryCatchThe ε }
Unconditional error recovery that ignores which exception was thrown. Usually used via the <|>
operator.
If both computations throw exceptions, then the result is the second exception.
Equations
- MonadExcept.orElse t₁ t₂ = tryCatch t₁ fun (x : ε) => t₂ ()
Instances For
Equations
- MonadExcept.instOrElse = { orElse := MonadExcept.orElse }
Adds the ability to access a read-only value of type ρ
to a monad. The value can be locally
overridden by withReader
, but it cannot be mutated.
Actions in the resulting monad are functions that take the local value as a parameter, returning
ordinary actions in m
.
Instances For
Equations
- ReaderT.instMonadLift = { monadLift := fun {α : Type ?u.16} (x : m α) (x_1 : ρ) => x }
Equations
- One or more equations did not get rendered due to their size.
Sequences two reader monad computations. Both are provided with the local value, and the second is
passed the value of the first. Typically used via the >>=
operator.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- ReaderT.instMonad = { toApplicative := ReaderT.instApplicativeOfMonad, bind := fun {α β : Type ?u.19} => ReaderT.bind }
Equations
- ReaderT.instMonadFunctor ρ m = { monadMap := fun {α : Type ?u.19} (f : {β : Type ?u.19} → m β → m β) (x : ReaderT ρ m α) (ctx : ρ) => f (x ctx) }
Modifies a reader monad's local value with f
. The resulting computation applies f
to the
incoming local value and passes the result to the inner computation.
Equations
- ReaderT.adapt f x r = x (f r)
Instances For
Reader monads provide the ability to implicitly thread a value through a computation. The value can
be read, but not written. A MonadWithReader ρ
instance additionally allows the value to be locally
overridden for a sub-computation.
In this class, ρ
is a semiOutParam
, which means that it can influence the choice of instance.
MonadReader ρ
provides the same operations, but requires that ρ
be inferrable from m
.
- read : m ρ
Retrieves the local value.
Instances
Reader monads provide the ability to implicitly thread a value through a computation. The value can
be read, but not written. A MonadWithReader ρ
instance additionally allows the value to be locally
overridden for a sub-computation.
In this class, ρ
is an outParam
, which means that it is inferred from m
. MonadReaderOf ρ
provides the same operations, but allows ρ
to influence instance synthesis.
- read : m ρ
Retrieves the local value.
Use
readThe
to explicitly specify a type when more than one value is available.
Instances
Retrieves the local value whose type is ρ
. This is useful when a monad supports reading more that
one type of value.
Use read
for a version that expects the type ρ
to be inferred from m
.
Equations
Instances For
Equations
- instMonadReaderOfMonadReaderOf ρ m = { read := readThe ρ }
Equations
- instMonadReaderOfOfMonadLift = { read := liftM read }
Equations
- instMonadReaderOfReaderTOfMonad = { read := ReaderT.read }
A reader monad that additionally allows the value to be locally overridden.
In this class, ρ
is a semiOutParam
, which means that it can influence the choice of instance.
MonadWithReader ρ
provides the same operations, but requires that ρ
be inferrable from m
.
Locally modifies the reader monad's value while running an action.
During the inner action
x
, reading the value returnsf
applied to the original value. After control returns fromx
, the reader monad's value is restored.
Instances
Locally modifies the reader monad's value while running an action, with the reader monad's local value type specified explicitly. This is useful when a monad supports reading more than one type of value.
During the inner action x
, reading the value returns f
applied to the original value. After
control returns from x
, the reader monad's value is restored.
Use withReader
for a version that expects the local value's type to be inferred from m
.
Equations
- withTheReader ρ f x = MonadWithReaderOf.withReader f x
Instances For
A reader monad that additionally allows the value to be locally overridden.
In this class, ρ
is an outParam
, which means that it is inferred from m
. MonadWithReaderOf ρ
provides the same operations, but allows ρ
to influence instance synthesis.
- withReader {α : Type u} : (ρ → ρ) → m α → m α
Locally modifies the reader monad's value while running an action.
During the inner action
x
, reading the value returnsf
applied to the original value. After control returns fromx
, the reader monad's value is restored.
Instances
Equations
- instMonadWithReaderOfMonadWithReaderOf ρ m = { withReader := fun {α : Type ?u.17} => withTheReader ρ }
Equations
- instMonadWithReaderOfOfMonadFunctor = { withReader := fun {α : Type ?u.28} (f : ρ → ρ) => monadMap fun {β : Type ?u.28} => withTheReader ρ f }
Equations
- instMonadWithReaderOfReaderT = { withReader := fun {α : Type ?u.18} (f : ρ → ρ) (x : ReaderT ρ m α) (ctx : ρ) => x (f ctx) }
State monads provide a value of a given type (the state) that can be retrieved or replaced.
Instances may implement these operations by passing state values around, by using a mutable
reference cell (e.g. ST.Ref σ
), or in other ways.
In this class, σ
is a semiOutParam
, which means that it can influence the choice of instance.
MonadState σ
provides the same operations, but requires that σ
be inferrable from m
.
The mutable state of a state monad is visible between multiple do
-blocks or functions, unlike
local mutable state in do
-notation.
- get : m σ
Retrieves the current value of the monad's mutable state.
- set : σ → m PUnit
Replaces the current value of the mutable state with a new one.
Applies a function to the current state that both computes a new state and a value. The new state replaces the current state, and the value is returned.
It is equivalent to
do let (a, s) := f (← get); set s; pure a
. However, usingmodifyGet
may lead to higher performance because it doesn't add a new reference to the state value. Additional references can inhibit in-place updates of data.
Instances
Gets the current state that has the explicitly-provided type σ
. When the current monad has
multiple state types available, this function selects one of them.
Equations
Instances For
Mutates the current state that has the explicitly-provided type σ
, replacing its value with the
result of applying f
to it. When the current monad has multiple state types available, this
function selects one of them.
It is equivalent to do set (f (← get))
. However, using modify
may lead to higher performance
because it doesn't add a new reference to the state value. Additional references can inhibit
in-place updates of data.
Equations
- modifyThe σ f = MonadStateOf.modifyGet fun (s : σ) => (PUnit.unit, f s)
Instances For
Applies a function to the current state that has the explicitly-provided type σ
. The function both
computes a new state and a value. The new state replaces the current state, and the value is
returned.
It is equivalent to do let (a, s) := f (← getThe σ); set s; pure a
. However, using modifyGetThe
may lead to higher performance because it doesn't add a new reference to the state value. Additional
references can inhibit in-place updates of data.
Equations
Instances For
State monads provide a value of a given type (the state) that can be retrieved or replaced.
Instances may implement these operations by passing state values around, by using a mutable
reference cell (e.g. ST.Ref σ
), or in other ways.
In this class, σ
is an outParam
, which means that it is inferred from m
. MonadStateOf σ
provides the same operations, but allows σ
to influence instance synthesis.
The mutable state of a state monad is visible between multiple do
-blocks or functions, unlike
local mutable state in do
-notation.
- get : m σ
Retrieves the current value of the monad's mutable state.
- set : σ → m PUnit
Replaces the current value of the mutable state with a new one.
Applies a function to the current state that both computes a new state and a value. The new state replaces the current state, and the value is returned.
It is equivalent to
do let (a, s) := f (← get); set s; pure a
. However, usingmodifyGet
may lead to higher performance because it doesn't add a new reference to the state value. Additional references can inhibit in-place updates of data.
Instances
Equations
- instMonadStateOfMonadStateOf σ m = { get := getThe σ, set := set, modifyGet := fun {α : Type ?u.19} (f : σ → α × σ) => MonadStateOf.modifyGet f }
Mutates the current state, replacing its value with the result of applying f
to it.
Use modifyThe
to explicitly select a state type to modify.
It is equivalent to do set (f (← get))
. However, using modify
may lead to higher performance
because it doesn't add a new reference to the state value. Additional references can inhibit
in-place updates of data.
Instances For
Equations
- instMonadStateOfOfMonadLift = { get := liftM MonadStateOf.get, set := fun (s : σ) => liftM (set s), modifyGet := fun {α : Type ?u.30} (f : σ → α × σ) => monadLift (modifyGet f) }
The value returned from a combined state and exception monad in which exceptions do not automatically roll back the state.
Result ε σ α
is equivalent to Except ε α × σ
, but using a single combined inductive type yields
a more efficient data representation.
- ok
{ε σ α : Type u}
: α → σ → Result ε σ α
A success value of type
α
and a new stateσ
. - error
{ε σ α : Type u}
: ε → σ → Result ε σ α
An exception of type
ε
and a new stateσ
.
Instances For
Equations
- EStateM.instInhabitedResult = { default := EStateM.Result.error default default }
A combined state and exception monad in which exceptions do not automatically roll back the state.
Instances of EStateM.Backtrackable
provide a way to roll back some part of the state if needed.
EStateM ε σ
is equivalent to ExceptT ε (StateM σ)
, but it is more efficient.
Equations
- EStateM ε σ α = (σ → EStateM.Result ε σ α)
Instances For
Equations
- EStateM.instInhabited = { default := fun (s : σ) => EStateM.Result.error default s }
Returns a value without modifying the state or throwing an exception.
Equations
- EStateM.pure a s = EStateM.Result.ok a s
Instances For
Replaces the current value of the mutable state with a new one.
Equations
- EStateM.set s x✝ = EStateM.Result.ok PUnit.unit s
Instances For
Retrieves the current value of the monad's mutable state.
Equations
- EStateM.get s = EStateM.Result.ok s s
Instances For
Applies a function to the current state that both computes a new state and a value. The new state replaces the current state, and the value is returned.
It is equivalent to do let (a, s) := f (← get); set s; pure a
. However, using modifyGet
may
lead to higher performance because it doesn't add a new reference to the state value. Additional
references can inhibit in-place updates of data.
Equations
- EStateM.modifyGet f s = match f s with | (a, s) => EStateM.Result.ok a s
Instances For
Throws an exception of type ε
to the nearest enclosing handler.
Equations
- EStateM.throw e s = EStateM.Result.error e s
Instances For
Exception handlers in EStateM
save some part of the state, determined by δ
, and restore it if an
exception is caught. By default, δ
is Unit
, and no information is saved.
- save : σ → δ
Extracts the information in the state that should be rolled back if an exception is handled.
- restore : σ → δ → σ
Updates the current state with the saved information that should be rolled back. This updated state becomes the current state when an exception is handled.
Instances
Handles exceptions thrown in the combined error and state monad.
The Backtrackable δ σ
instance is used to save a snapshot of part of the state prior to running
x
. If an exception is caught, the state is updated with the saved snapshot, rolling back part of
the state. If no instance of Backtrackable
is provided, a fallback instance in which δ
is Unit
is used, and no information is rolled back.
Equations
- x.tryCatch handle s = match x s with | EStateM.Result.error e s_1 => handle e (EStateM.Backtrackable.restore s_1 (EStateM.Backtrackable.save s)) | ok => ok
Instances For
Failure handling that does not depend on specific exception values.
The Backtrackable δ σ
instance is used to save a snapshot of part of the state prior to running
x₁
. If an exception is caught, the state is updated with the saved snapshot, rolling back part of
the state. If no instance of Backtrackable
is provided, a fallback instance in which δ
is Unit
is used, and no information is rolled back.
Equations
- x₁.orElse x₂ s = match x₁ s with | EStateM.Result.error a s_1 => x₂ () (EStateM.Backtrackable.restore s_1 (EStateM.Backtrackable.save s)) | ok => ok
Instances For
Transforms exceptions with a function, doing nothing on successful results.
Equations
- EStateM.adaptExcept f x s = match x s with | EStateM.Result.error e s => EStateM.Result.error (f e) s | EStateM.Result.ok a s => EStateM.Result.ok a s
Instances For
Sequences two EStateM ε σ
actions, passing the returned value from the first into the second.
Equations
- x.bind f s = match x s with | EStateM.Result.ok a s => f a s | EStateM.Result.error e s => EStateM.Result.error e s
Instances For
Transforms the value returned from an EStateM ε σ
action using a function.
Equations
- EStateM.map f x s = match x s with | EStateM.Result.ok a s => EStateM.Result.ok (f a) s | EStateM.Result.error e s => EStateM.Result.error e s
Instances For
Sequences two EStateM ε σ
actions, running x
before y
. The first action's return value is
ignored.
Equations
- x.seqRight y s = match x s with | EStateM.Result.ok a s => y () s | EStateM.Result.error e s => EStateM.Result.error e s
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- EStateM.instOrElseOfBacktrackable = { orElse := EStateM.orElse }
Equations
- EStateM.instMonadStateOf = { get := EStateM.get, set := EStateM.set, modifyGet := fun {α : Type ?u.12} => EStateM.modifyGet }
Equations
- EStateM.instMonadExceptOfOfBacktrackable = { throw := fun {α : Type ?u.23} => EStateM.throw, tryCatch := fun {α : Type ?u.23} => EStateM.tryCatch }
Executes an EStateM
with the initial state s
for the returned value α
, discarding the final
state. Returns none
if an unhandled exception was thrown.
Equations
- x.run' s = match x.run s with | EStateM.Result.ok v a => some v | EStateM.Result.error a a_1 => none
Instances For
The restore
implementation for Backtrackable PUnit σ
.
Equations
- EStateM.dummyRestore s x✝ = s
Instances For
A fallback Backtrackable
instance that saves no information from a state. This allows every type
to be used as a state in EStateM
, with no rollback.
Because this is the first declared instance of Backtrackable _ σ
, it will be picked only if there
are no other Backtrackable _ σ
instances registered.
Equations
- EStateM.nonBacktrackable = { save := EStateM.dummySave, restore := EStateM.dummyRestore }
Computes a hash for strings.
Equations
- instHashableString = { hash := String.hash }
A hash function for names, which is stored inside the name itself as a computed field.
Equations
- Lean.Name.anonymous.hash = UInt64.ofNatLT 1723 Lean.Name.hash.proof_3
- (p.str s).hash = mixHash p.hash s.hash
- (p.num v).hash = mixHash p.hash (if h : v < UInt64.size then UInt64.ofNatLT v h else UInt64.ofNatLT 17 Lean.Name.hash.proof_4)
Instances For
Hierarchical names consist of a sequence of components, each of
which is either a string or numeric, that are written separated by dots (.
).
Hierarchical names are used to name declarations and for creating unique identifiers for free variables and metavariables.
You can create hierarchical names using a backtick:
`Lean.Meta.whnf
It is short for .str (.str (.str .anonymous "Lean") "Meta") "whnf"
.
You can use double backticks to request Lean to statically check whether the name corresponds to a Lean declaration in scope.
``Lean.Meta.whnf
If the name is not in scope, Lean will report an error.
There are two ways to convert a String
to a Name
:
Name.mkSimple
creates a name with a single string component.String.toName
first splits the string into its dot-separated components, and then creates a hierarchical name.
- anonymous : Name
The "anonymous" name.
- str (pre : Name) (str : String) : Name
- num (pre : Name) (i : Nat) : Name
Instances For
Equations
- Lean.instInhabitedName = { default := Lean.Name.anonymous }
Equations
- Lean.instHashableName = { hash := Lean.Name.hash }
Make name s₁
Equations
Instances For
Make name s₁.s₂
Equations
- Lean.Name.mkStr2 s₁ s₂ = (Lean.Name.anonymous.str s₁).str s₂
Instances For
Make name s₁.s₂.s₃
Equations
- Lean.Name.mkStr3 s₁ s₂ s₃ = ((Lean.Name.anonymous.str s₁).str s₂).str s₃
Instances For
Make name s₁.s₂.s₃.s₄
Equations
- Lean.Name.mkStr4 s₁ s₂ s₃ s₄ = (((Lean.Name.anonymous.str s₁).str s₂).str s₃).str s₄
Instances For
Make name s₁.s₂.s₃.s₄.s₅
Equations
- Lean.Name.mkStr5 s₁ s₂ s₃ s₄ s₅ = ((((Lean.Name.anonymous.str s₁).str s₂).str s₃).str s₄).str s₅
Instances For
Make name s₁.s₂.s₃.s₄.s₅.s₆
Equations
- Lean.Name.mkStr6 s₁ s₂ s₃ s₄ s₅ s₆ = (((((Lean.Name.anonymous.str s₁).str s₂).str s₃).str s₄).str s₅).str s₆
Instances For
Make name s₁.s₂.s₃.s₄.s₅.s₆.s₇
Equations
- Lean.Name.mkStr7 s₁ s₂ s₃ s₄ s₅ s₆ s₇ = ((((((Lean.Name.anonymous.str s₁).str s₂).str s₃).str s₄).str s₅).str s₆).str s₇
Instances For
Make name s₁.s₂.s₃.s₄.s₅.s₆.s₇.s₈
Equations
Instances For
(Boolean) equality comparator for names.
Equations
Instances For
This function does not have special support for macro scopes.
See Name.append
.
Equations
- x✝.appendCore Lean.Name.anonymous = x✝
- x✝.appendCore (p.str s) = (x✝.appendCore p).str s
- x✝.appendCore (p.num d) = (x✝.appendCore p).num d
Instances For
The default maximum recursion depth. This is adjustable using the maxRecDepth
option.
Equations
Instances For
The message to display on stack overflow.
Equations
- Lean.maxRecDepthErrorMessage = "maximum recursion depth has been reached\nuse `set_option maxRecDepth <num>` to increase limit\nuse `set_option diagnostics true` to get diagnostic information"
Instances For
Syntax #
Source information that relates syntax to the context that it came from.
The primary purpose of SourceInfo
is to relate the output of the parser and the macro expander to
the original source file. When produced by the parser, Syntax.node
does not carry source info; the
parser associates it only with atoms and identifiers. If a Syntax.node
is introduced by a
quotation, then it has synthetic source info that both associates it with an original reference
position and indicates that the original atoms in it may not originate from the Lean file under
elaboration.
Source info is also used to relate Lean's output to the internal data that it represents; this is
the basis for many interactive features. When used this way, it can occur on Syntax.node
as well.
- original
(leading : Substring)
(pos : String.Pos)
(trailing : Substring)
(endPos : String.Pos)
: SourceInfo
A token produced by the parser from original input that includes both leading and trailing whitespace as well as position information.
The
leading
whitespace is inferred after parsing bySyntax.updateLeading
. This is because the “preceding token” is not well-defined during parsing, especially in the presence of backtracking. - synthetic
(pos endPos : String.Pos)
(canonical : Bool := false)
: SourceInfo
Synthetic syntax is syntax that was produced by a metaprogram or by Lean itself (e.g. by a quotation). Synthetic syntax is annotated with a source span from the original syntax, which relates it to the source file.
The delaborator uses this constructor to store an encoded indicator of which core language expression gave rise to the syntax.
The
canonical
flag on synthetic syntax is enabled for syntax that is not literally part of the original input syntax but should be treated “as if” the user really wrote it for the purpose of hovers and error messages. This is usually used on identifiers in order to connect the binding site to the user's original syntax even if the name of the identifier changes during expansion, as well as on tokens that should receive targeted messages.Generally speaking, a macro expansion should only use a given piece of input syntax in a single canonical token. An exception to this rule is when the same identifier is used to declare two binders, as in the macro expansion for dependent if:
`(if $h : $cond then $t else $e) ~> `(dite $cond (fun $h => $t) (fun $h => $t))
In these cases, if the user hovers over
h
they will see information about both binding sites. - none : SourceInfo
A synthesized token without position information.
Instances For
Equations
- Lean.instInhabitedSourceInfo = { default := Lean.SourceInfo.none }
Gets the position information from a SourceInfo
, if available.
If canonicalOnly
is true, then .synthetic
syntax with canonical := false
will also return none
.
Equations
Instances For
Gets the end position information from a SourceInfo
, if available.
If canonicalOnly
is true, then .synthetic
syntax with canonical := false
will also return none
.
Equations
- (Lean.SourceInfo.original leading pos trailing endPos).getTailPos? canonicalOnly = some endPos
- (Lean.SourceInfo.synthetic pos endPos true).getTailPos? canonicalOnly = some endPos
- (Lean.SourceInfo.synthetic pos endPos canonical).getTailPos? = some endPos
- info.getTailPos? canonicalOnly = none
Instances For
Gets the substring representing the trailing whitespace of a SourceInfo
, if available.
Equations
- (Lean.SourceInfo.original leading pos trailing endPos).getTrailing? = some trailing
- info.getTrailing? = none
Instances For
Gets the end position information of the trailing whitespace of a SourceInfo
, if available.
If canonicalOnly
is true, then .synthetic
syntax with canonical := false
will also return none
.
Equations
- info.getTrailingTailPos? canonicalOnly = match info.getTrailing? with | some trailing => some trailing.stopPos | none => info.getTailPos? canonicalOnly
Instances For
Specifies the interpretation of a Syntax.node
value. An abbreviation for Name
.
Node kinds may be any name, and do not need to refer to declarations in the environment.
Conventionally, however, a node's kind corresponds to the Parser
or ParserDesc
declaration that
produces it. There are also a number of built-in node kinds that are used by the parsing
infrastructure, such as nullKind
and choiceKind
; these do not correspond to parser declarations.
Equations
Instances For
Syntax AST #
A possible binding of an identifier in the context in which it was quoted.
Identifiers in quotations may refer to either global declarations or to namespaces that are in scope
at the site of the quotation. These are saved in the Syntax.ident
constructor and are part of the
implementation of hygienic macros.
- namespace
(ns : Name)
: Preresolved
A potential namespace reference
- decl
(n : Name)
(fields : List String)
: Preresolved
A potential global constant or section variable reference, with additional field accesses
Instances For
Lean syntax trees.
Syntax trees are used pervasively throughout Lean: they are produced by the parser, transformed by the macro expander, and elaborated. They are also produced by the delaborator and presented to users.
- missing : Syntax
A portion of the syntax tree that is missing because of a parse error.
The indexing operator on
Syntax
also returnsSyntax.missing
when the index is out of bounds. - node
(info : SourceInfo)
(kind : SyntaxNodeKind)
(args : Array Syntax)
: Syntax
A node in the syntax tree that may have further syntax as child nodes. The node's
kind
determines its interpretation.For nodes produced by the parser, the
info
field is typicallyLean.SourceInfo.none
, and source information is stored in the corresponding fields of identifiers and atoms. This field is used in two ways:- The delaborator uses it to associate nodes with metadata that are used to implement interactive features.
- Nodes created by quotations use the field to mark the syntax as synthetic (storing the result
of
Lean.SourceInfo.fromRef
) even when its leading or trailing tokens are not.
- atom
(info : SourceInfo)
(val : String)
: Syntax
A non-identifier atomic component of syntax.
All of the following are atoms:
- keywords, such as
def
,fun
, andinductive
- literals, such as numeric or string literals
- punctuation and delimiters, such as
(
,)
, and=>
.
Identifiers are represented by the
Lean.Syntax.ident
constructor. Atoms also correspond to quoted strings insidesyntax
declarations. - keywords, such as
- ident
(info : SourceInfo)
(rawVal : Substring)
(val : Name)
(preresolved : List Preresolved)
: Syntax
An identifier.
In addition to source information, identifiers have the following fields:
rawVal
is the literal substring from the input fileval
is the parsed Lean name, potentially including macro scopes.preresolved
is the list of possible declarations this could refer to, populated by quotations.
Instances For
Create syntax node with 1 child
Equations
- Lean.Syntax.node1 info kind a₁ = Lean.Syntax.node info kind #[a₁]
Instances For
Create syntax node with 2 children
Equations
- Lean.Syntax.node2 info kind a₁ a₂ = Lean.Syntax.node info kind #[a₁, a₂]
Instances For
Create syntax node with 3 children
Equations
- Lean.Syntax.node3 info kind a₁ a₂ a₃ = Lean.Syntax.node info kind #[a₁, a₂, a₃]
Instances For
Create syntax node with 4 children
Equations
- Lean.Syntax.node4 info kind a₁ a₂ a₃ a₄ = Lean.Syntax.node info kind #[a₁, a₂, a₃, a₄]
Instances For
Create syntax node with 5 children
Equations
- Lean.Syntax.node5 info kind a₁ a₂ a₃ a₄ a₅ = Lean.Syntax.node info kind #[a₁, a₂, a₃, a₄, a₅]
Instances For
Create syntax node with 6 children
Equations
- Lean.Syntax.node6 info kind a₁ a₂ a₃ a₄ a₅ a₆ = Lean.Syntax.node info kind #[a₁, a₂, a₃, a₄, a₅, a₆]
Instances For
Create syntax node with 7 children
Equations
Instances For
Create syntax node with 8 children
Equations
Instances For
SyntaxNodeKinds
is a set of SyntaxNodeKind
, implemented as a list.
Singleton SyntaxNodeKinds
are extremely common. They are written as name literals, rather than as
lists; list syntax is required only for empty or non-singleton sets of kinds.
Equations
Instances For
Equations
- Lean.instInhabitedSyntax = { default := Lean.Syntax.missing }
Equations
- Lean.instInhabitedTSyntax = { default := { raw := default } }
Builtin kinds #
The `choice
kind is used to represent ambiguous parse results.
The parser prioritizes longer matches over shorter ones, but there is not always a unique longest match. All the parse results are saved, and the determination of which to use is deferred until typing information is available.
Equations
- Lean.choiceKind = `choice
Instances For
`null
is the “fallback” kind, used when no other kind applies. Null nodes result from
repetition operators, and empty null nodes represent the failure of an optional parse.
The null kind is used for raw list parsers like many
.
Equations
- Lean.nullKind = `null
Instances For
The `group
kind is used for nodes that result from Lean.Parser.group
. This avoids confusion
with the null kind when used inside optional
.
Equations
- Lean.groupKind = `group
Instances For
The pseudo-kind assigned to identifiers: `ident
.
The name `ident
is not actually used as a kind for Syntax.node
values. It is used by
convention as the kind of Syntax.ident
values.
Equations
- Lean.identKind = `ident
Instances For
`str
is the node kind of string literals like "foo"
.
Equations
- Lean.strLitKind = `str
Instances For
`char
is the node kind of character literals like 'A'
.
Equations
- Lean.charLitKind = `char
Instances For
`num
is the node kind of number literals like 42
.
Equations
- Lean.numLitKind = `num
Instances For
`scientific
is the node kind of floating point literals like 1.23e-3
.
Equations
- Lean.scientificLitKind = `scientific
Instances For
`name
is the node kind of name literals like `foo
.
Equations
- Lean.nameLitKind = `name
Instances For
`` fieldIdx
is the node kind of projection indices like the 2
in x.2
.
Equations
- Lean.fieldIdxKind = `fieldIdx
Instances For
`hygieneInfo
is the node kind of the Lean.Parser.hygieneInfo
parser, which produces an
“invisible token” that captures the hygiene information at the current point without parsing
anything.
They can be used to generate identifiers (with Lean.HygieneInfo.mkIdent
) as if they were
introduced in a macro's input, rather than by its implementation.
Equations
- Lean.hygieneInfoKind = `hygieneInfo
Instances For
`interpolatedStrLitKind
is the node kind of interpolated string literal
fragments like "value = {
and }"
in s!"value = {x}"
.
Equations
- Lean.interpolatedStrLitKind = `interpolatedStrLitKind
Instances For
`interpolatedStrKind
is the node kind of an interpolated string literal like "value = {x}"
in s!"value = {x}"
.
Equations
- Lean.interpolatedStrKind = `interpolatedStrKind
Instances For
Creates an info-less node of the given kind and children.
Equations
- Lean.mkNode k args = { raw := Lean.Syntax.node Lean.SourceInfo.none k args }
Instances For
Creates an info-less nullKind
node with the given children, if any.
Equations
- Lean.mkNullNode args = (Lean.mkNode Lean.nullKind args).raw
Instances For
Gets the kind of a Syntax.node
value, or the pseudo-kind of any other Syntax
value.
“Pseudo-kinds” are kinds that are assigned by convention to non-Syntax.node
values:
identKind
for Syntax.ident
, `missing
for Syntax.missing
, and the atom's string literal
for atoms.
Equations
- (Lean.Syntax.node info k args).getKind = k
- Lean.Syntax.missing.getKind = `missing
- (Lean.Syntax.atom info v).getKind = Lean.Name.mkSimple v
- (Lean.Syntax.ident info rawVal val preresolved).getKind = Lean.identKind
Instances For
Changes the kind at the root of a Syntax.node
to k
.
Returns all other Syntax
values unchanged.
Equations
- (Lean.Syntax.node info kind args).setKind k = Lean.Syntax.node info k args
- stx.setKind k = stx
Instances For
Checks whether syntax has the given kind or pseudo-kind.
“Pseudo-kinds” are kinds that are assigned by convention to non-Syntax.node
values:
identKind
for Syntax.ident
, `missing
for Syntax.missing
, and the atom's string literal
for atoms.
Instances For
Gets the i
'th argument of the syntax node. This can also be written stx[i]
.
Returns missing
if i
is out of range.
Equations
- (Lean.Syntax.node info kind args).getArg i = args.getD i Lean.Syntax.missing
- stx.getArg i = Lean.Syntax.missing
Instances For
Gets the number of arguments of the syntax node, or 0
if it's not a node
.
Equations
- (Lean.Syntax.node info kind args).getNumArgs = args.size
- stx.getNumArgs = 0
Instances For
Assuming stx
was parsed by optional
, returns the enclosed syntax
if it parsed something and none
otherwise.
Equations
- (Lean.Syntax.node info kind args).getOptional? = match kind == Lean.nullKind && args.size == 1 with | true => some (args.get!Internal 0) | false => none
- stx.getOptional? = none
Instances For
Is this syntax a node
with kind k
?
Instances For
If this is an ident
, return the parsed value, else .anonymous
.
Equations
- (Lean.Syntax.ident info rawVal val preresolved).getId = val
- x✝.getId = Lean.Name.anonymous
Instances For
Retrieve the immediate info from the Syntax node.
Equations
- (Lean.Syntax.atom info val).getInfo? = some info
- (Lean.Syntax.ident info rawVal val preresolved).getInfo? = some info
- (Lean.Syntax.node info kind args).getInfo? = some info
- Lean.Syntax.missing.getInfo? = none
Instances For
Retrieve the left-most node or leaf's info in the Syntax tree.
Retrieve the left-most leaf's info in the Syntax tree, or none
if there is no token.
Equations
- stx.getHeadInfo = match stx.getHeadInfo? with | some info => info | none => Lean.SourceInfo.none
Instances For
Get the starting position of the syntax, if possible.
If canonicalOnly
is true, non-canonical synthetic
nodes are treated as not carrying
position information.
Equations
- stx.getPos? canonicalOnly = stx.getHeadInfo.getPos? canonicalOnly
Instances For
Get the ending position of the syntax, if possible.
If canonicalOnly
is true, non-canonical synthetic
nodes are treated as not carrying
position information.
An array of syntax elements interspersed with the given separators.
Separator arrays result from repetition operators such as ,*
.
Coercions to and from Array Syntax
insert or remove separators
as required.
The typed equivalent is Lean.Syntax.TSepArray
.
The array of elements and separators, ordered like
#[el1, sep1, el2, sep2, el3]
.
Instances For
An array of syntax elements that alternate with the given separator. Each syntax element has a kind
drawn from ks
.
Separator arrays result from repetition operators such as ,*
.
Coercions to and from Array (TSyntax ks)
insert or remove
separators as required. The untyped equivalent is Lean.Syntax.SepArray
.
The array of elements and separators, ordered like
#[el1, sep1, el2, sep2, el3]
.
Instances For
An array of syntaxes of kind ks
.
Equations
- Lean.TSyntaxArray ks = Array (Lean.TSyntax ks)
Instances For
Converts a TSyntaxArray
to an Array Syntax
, without reallocation.
Converts an Array Syntax
to a TSyntaxArray
, without reallocation.
Constructs a synthetic SourceInfo
using a ref : Syntax
for the span.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Constructs a synthetic atom
with source info coming from src
.
Equations
- Lean.mkAtomFrom src val canonical = Lean.Syntax.atom (Lean.SourceInfo.fromRef src canonical) val
Instances For
Parser descriptions #
A ParserDescr
is a grammar for parsers. This is used by the syntax
command
to produce parsers without having to import Lean
.
- const
(name : Name)
: ParserDescr
A (named) nullary parser, like
ppSpace
- unary
(name : Name)
(p : ParserDescr)
: ParserDescr
A (named) unary parser, like
group(p)
- binary
(name : Name)
(p₁ p₂ : ParserDescr)
: ParserDescr
A (named) binary parser, like
orelse
orandthen
(written asp1 <|> p2
andp1 p2
respectively insyntax
) - node
(kind : SyntaxNodeKind)
(prec : Nat)
(p : ParserDescr)
: ParserDescr
Parses using
p
, then pops the stack to create a new node with kindkind
. The precedenceprec
is used to determine whether the parser should apply given the current precedence level. - trailingNode
(kind : SyntaxNodeKind)
(prec lhsPrec : Nat)
(p : ParserDescr)
: ParserDescr
Like
node
but for trailing parsers (which start with a nonterminal). Assumes the lhs is already on the stack, and parses usingp
, then pops the stack including the lhs to create a new node with kindkind
. The precedenceprec
andlhsPrec
are used to determine whether the parser should apply. - symbol (val : String) : ParserDescr
- nonReservedSymbol (val : String) (includeIdent : Bool) : ParserDescr
- cat
(catName : Name)
(rbp : Nat)
: ParserDescr
Parses using the category parser
catName
with right binding power (i.e. precedence)rbp
. - parser
(declName : Name)
: ParserDescr
Parses using another parser
declName
, which can be either aParser
orParserDescr
. - nodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : ParserDescr) : ParserDescr
- sepBy
(p : ParserDescr)
(sep : String)
(psep : ParserDescr)
(allowTrailingSep : Bool := false)
: ParserDescr
A
sepBy(p, sep)
parses 0 or more occurrences ofp
separated bysep
.psep
is usually the same assymbol sep
, but it can be overridden.sep
is only used in the antiquot syntax:$x;*
would match ifsep
is";"
.allowTrailingSep
is true if e.g.a, b,
is also allowed to match. - sepBy1 (p : ParserDescr) (sep : String) (psep : ParserDescr) (allowTrailingSep : Bool := false) : ParserDescr
Instances For
Equations
- Lean.instInhabitedParserDescr = { default := Lean.ParserDescr.symbol "" }
Although TrailingParserDescr
is an abbreviation for ParserDescr
, Lean will
look at the declared type in order to determine whether to add the parser to
the leading or trailing parser table. The determination is done automatically
by the syntax
command.
Equations
Instances For
Runtime support for making quotation terms auto-hygienic, by mangling identifiers introduced by them with a "macro scope" supplied by the context. Details to appear in a paper soon.
A macro scope identifier is just a Nat
that gets bumped every time we
enter a new macro scope. Within a macro scope, all occurrences of identifier x
parse to the same thing, but x
parsed from different macro scopes will
produce different identifiers.
Equations
Instances For
Macro scope used internally. It is not available for our frontend.
Equations
Instances For
First macro scope available for our frontend
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Run x : m α
with a modified value for the ref
. This is not exactly
the same as MonadRef.withRef
, because it uses replaceRef
to avoid putting
syntax with bad spans in the state.
Equations
- Lean.withRef ref x = do let oldRef ← Lean.getRef let ref : Lean.Syntax := Lean.replaceRef ref oldRef Lean.MonadRef.withRef ref x
Instances For
If ref? = some ref
, run x : m α
with a modified value for the ref
by calling withRef
.
Otherwise, run x
directly.
Equations
- Lean.withRef? (some ref) x = Lean.withRef ref x
- Lean.withRef? ref? x = x
Instances For
A monad that supports syntax quotations. Syntax quotations (in term
position) are monadic values that when executed retrieve the current "macro
scope" from the monad and apply it to every identifier they introduce
(independent of whether this identifier turns out to be a reference to an
existing declaration, or an actually fresh binding during further
elaboration). We also apply the position of the result of getRef
to each
introduced symbol, which results in better error positions than not applying
any position.
- getCurrMacroScope : m MacroScope
Get the fresh scope of the current macro invocation
- getMainModule : m Name
Get the module name of the current file. This is used to ensure that hygienic names don't clash across multiple files.
- withFreshMacroScope {α : Type} : m α → m α
Execute action in a new macro invocation context. This transformer should be used at all places that morally qualify as the beginning of a "macro call", e.g.
elabCommand
andelabTerm
in the case of the elaborator. However, it can also be used internally inside a "macro" if identifiers introduced by e.g. different recursive calls should be independent and not collide. While returning an intermediate syntax tree that will recursively be expanded by the elaborator can be used for the same effect, doing direct recursion inside the macro guarded by this transformer is often easier because one is not restricted to passing a single syntax tree. Modelling this helper as a transformer and not just a monadic action ensures that the current macro scope before the recursive call is restored after it, as expected.
Instances
Construct a synthetic SourceInfo
from the ref
in the monad state.
Equations
- Lean.MonadRef.mkInfoFromRefPos = do let __do_lift ← Lean.getRef pure (Lean.SourceInfo.fromRef __do_lift)
Instances For
Equations
- One or more equations did not get rendered due to their size.
We represent a name with macro scopes as
<actual name>._@.(<module_name>.<scopes>)*.<module_name>._hyg.<scopes>
Example: suppose the module name is Init.Data.List.Basic
, and name is foo.bla
, and macroscopes [2, 5]
foo.bla._@.Init.Data.List.Basic._hyg.2.5
We may have to combine scopes from different files/modules. The main modules being processed is always the right-most one. This situation may happen when we execute a macro generated in an imported file in the current file.
foo.bla._@.Init.Data.List.Basic.2.1.Init.Lean.Expr._hyg.4
The delimiter _hyg
is used just to improve the hasMacroScopes
performance.
Does this name have hygienic macro scopes?
Equations
- (pre.str s).hasMacroScopes = (s == "_hyg")
- (p.num i).hasMacroScopes = p.hasMacroScopes
- x✝.hasMacroScopes = false
Instances For
Remove the macro scopes from the name.
Equations
- n.eraseMacroScopes = match n.hasMacroScopes with | true => Lean.eraseMacroScopesAux✝ n | false => n
Instances For
Helper function we use to create binder names that do not need to be unique.
Equations
- n.simpMacroScopes = match n.hasMacroScopes with | true => Lean.simpMacroScopesAux✝ n | false => n
Instances For
A MacroScopesView
represents a parsed hygienic name. extractMacroScopes
will decode it from a Name
, and .review
will re-encode it. The grammar of a
hygienic name is:
<name>._@.(<module_name>.<scopes>)*.<mainModule>._hyg.<scopes>
- name : Name
The original (unhygienic) name.
- imported : Name
All the name components
(<module_name>.<scopes>)*
from the imports concatenated together. - mainModule : Name
The main module in which this identifier was parsed.
- scopes : List MacroScope
The list of macro scopes.
Instances For
Encode a hygienic name from the parsed pieces.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Revert all addMacroScope
calls. v = extractMacroScopes n → n = v.review
.
This operation is useful for analyzing/transforming the original identifiers, then adding back
the scopes (via MacroScopesView.review
).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Add a new macro scope onto the name n
, in the given mainModule
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Appends two names a
and b
, propagating macro scopes from a
or b
, if any, to the result.
Panics if both a
and b
have macro scopes.
This function is used for the Append Name
instance.
See also Lean.Name.appendCore
, which appends names without any consideration for macro scopes.
Also consider Lean.Name.eraseMacroScopes
to erase macro scopes before appending, if appropriate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.instAppendName = { append := Lean.Name.append }
Add a new macro scope onto the name n
, using the monad state to supply the
main module and current macro scope.
Equations
- Lean.MonadQuotation.addMacroScope n = do let mainModule ← Lean.getMainModule let scp ← Lean.getCurrMacroScope pure (Lean.addMacroScope mainModule n scp)
Instances For
Function used for determining whether a syntax pattern `(id)
is matched.
There are various conceivable notions of when two syntactic identifiers should be regarded as identical,
but semantic definitions like whether they refer to the same global name cannot be implemented without
context information (i.e. MonadResolveName
). Thus in patterns we default to the structural solution
of comparing the identifiers' Name
values, though we at least do so modulo macro scopes so that
identifiers that "look" the same match. This is particularly useful when dealing with identifiers that
do not actually refer to Lean bindings, e.g. in the stx
pattern `(many($p))
.
Equations
- stx.matchesIdent id = (stx.isIdent && stx.getId.eraseMacroScopes == id.eraseMacroScopes)
Instances For
Is this syntax a node kind k
wrapping an atom _ val
?
Equations
- (Lean.Syntax.node info kind args).matchesLit k val = (k == kind && match args.getD 0 Lean.Syntax.missing with | Lean.Syntax.atom info val' => val == val' | x => false)
- stx.matchesLit k val = false
Instances For
The read-only context for the MacroM
monad.
- methods : Lean.Macro.MethodsRef✝
- mainModule : Name
The currently parsing module.
- currMacroScope : MacroScope
The current macro scope.
- currRecDepth : Nat
The current recursion depth.
- maxRecDepth : Nat
The maximum recursion depth.
- ref : Syntax
The syntax which supplies the position of error messages.
Instances For
An exception in the MacroM
monad.
- error : Syntax → String → Exception
A general error, given a message and a span (expressed as a
Syntax
). - unsupportedSyntax : Exception
An unsupported syntax exception. We keep this separate because it is used for control flow: if one macro does not support a syntax then we try the next one.
Instances For
The mutable state for the MacroM
monad.
- macroScope : MacroScope
The global macro scope counter, used for producing fresh scope names.
The list of trace messages that have been produced, each with a trace class and a message.
Instances For
Equations
- Lean.Macro.instInhabitedState = { default := { macroScope := default, traceMsgs := default } }
The MacroM
monad is the main monad for macro expansion. It has the
information needed to handle hygienic name generation, and is the monad that
macro
definitions live in.
Notably, this is a (relatively) pure monad: there is no IO
and no access to
the Environment
. That means that things like declaration lookup are
impossible here, as well as IO.Ref
or other side-effecting operations.
For more capabilities, macros can instead be written as elab
using adaptExpander
.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Add a new macro scope to the name n
.
Equations
- Lean.Macro.addMacroScope n = do let ctx ← read pure (Lean.addMacroScope ctx.mainModule n ctx.currMacroScope)
Instances For
Throw an unsupportedSyntax
exception.
Instances For
Throw an error with the given message,
using the ref
for the location information.
Equations
- Lean.Macro.throwError msg = do let ref ← Lean.getRef throw (Lean.Macro.Exception.error ref msg)
Instances For
Throw an error with the given message and location information.
Equations
- Lean.Macro.throwErrorAt ref msg = Lean.withRef ref (Lean.Macro.throwError msg)
Instances For
Increments the macro scope counter so that inside the body of x
the macro
scope is fresh.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Implementation of mkMethods
.
Equations
- Lean.Macro.mkMethodsImp methods = unsafeCast methods
Instances For
Make an opaque reference to a Methods
.
Equations
- Lean.Macro.instInhabitedMethodsRef = { default := Lean.Macro.mkMethods default }
Implementation of getMethods
.
Equations
- Lean.Macro.getMethodsImp = do let ctx ← read pure (unsafeCast ctx.methods)
Instances For
Extract the methods list from the MacroM
state.
expandMacro? stx
returns some stxNew
if stx
is a macro,
and stxNew
is its expansion.
Equations
- Lean.expandMacro? stx = do let __do_lift ← Lean.Macro.getMethods __do_lift.expandMacro? stx
Instances For
Returns true
if the environment contains a declaration with name declName
Equations
- Lean.Macro.hasDecl declName = do let __do_lift ← Lean.Macro.getMethods __do_lift.hasDecl declName
Instances For
Gets the current namespace given the position in the file.
Equations
- Lean.Macro.getCurrNamespace = do let __do_lift ← Lean.Macro.getMethods __do_lift.getCurrNamespace
Instances For
Resolves the given name to an overload list of namespaces.
Equations
- Lean.Macro.resolveNamespace n = do let __do_lift ← Lean.Macro.getMethods __do_lift.resolveNamespace n
Instances For
Resolves the given name to an overload list of global definitions.
The List String
in each alternative is the deduced list of projections
(which are ambiguous with name components).
Remark: it will not trigger actions associated with reserved names. Recall that Lean
has reserved names. For example, a definition foo
has a reserved name foo.def
for theorem
containing stating that foo
is equal to its definition. The action associated with foo.def
automatically proves the theorem. At the macro level, the name is resolved, but the action is not
executed. The actions are executed by the elaborator when converting Syntax
into Expr
.
Equations
- Lean.Macro.resolveGlobalName n = do let __do_lift ← Lean.Macro.getMethods __do_lift.resolveGlobalName n
Instances For
Add a new trace message, with the given trace class and message.
Equations
- Lean.Macro.trace clsName msg = modify fun (s : Lean.Macro.State) => { macroScope := s.macroScope, traceMsgs := (clsName, msg) :: s.traceMsgs }
Instances For
Function that tries to reverse macro expansions as a post-processing step of delaboration.
While less general than an arbitrary delaborator, it can be declared without importing Lean
.
Used by the [app_unexpander]
attribute.
Instances For
Equations
- One or more equations did not get rendered due to their size.