- natVal: Nat → Lean.Literal
Natural number literal
- strVal: String → Lean.Literal
String literal
Literal values for Expr
.
Instances For
Total order on Expr
literal values.
Natural number values are smaller than string literal values.
Instances For
- default: Lean.BinderInfo
Default binder annotation, e.g.
(x : α)
- implicit: Lean.BinderInfo
Implicit binder annotation, e.g.,
{x : α}
- strictImplicit: Lean.BinderInfo
Strict implict binder annotation, e.g.,
{{ x : α }}
- instImplicit: Lean.BinderInfo
Local instance binder annotataion, e.g.,
[Decidable α]
Arguments in forallE binders can be labelled as implicit or explicit.
Each lam
or forallE
binder comes with a binderInfo
argument (stored in ExprData).
This can be set to
default
--(x : α)
implicit
--{x : α}
strict_implicit
--⦃x : α⦄
inst_implicit
--[x : α]
.aux_decl
-- Auxillary definitions are helper methods that Lean generates.aux_decl
is used for_match
,_fun_match
,_let_match
and the self reference that appears in recursive pattern matching.
The difference between implicit {}
and strict-implicit ⦃⦄
is how
implicit arguments are treated that are not followed by explicit arguments.
{}
arguments are applied eagerly, while ⦃⦄
arguments are left partially applied:
def foo {x : Nat} : Nat := x
def bar ⦃x : Nat⦄ : Nat := x
#check foo -- foo : Nat
#check bar -- bar : ⦃x : Nat⦄ → Nat
See also the Lean manual: https://leanprover.github.io/lean4/doc/expressions.html#implicit-arguments
Instances For
Return true
if the given BinderInfo
does not correspond to an implicit binder annotation
(i.e., implicit
, strictImplicit
, or instImplicit
).
Instances For
Return true
if the given BinderInfo
is an instance implicit annotation (e.g., [Decidable α]
)
Instances For
Return true
if the given BinderInfo
is a regular implicit annotation (e.g., {α : Type u}
)
Instances For
Return true
if the given BinderInfo
is a strict implicit annotation (e.g., {{α : Type u}}
)
Instances For
Cached hash code, cached results, and other data for Expr
.
- hash : 32-bits
- approxDepth : 8-bits -- the approximate depth is used to minimize the number of hash collisions
- hasFVar : 1-bit -- does it contain free variables?
- hasExprMVar : 1-bit -- does it contain metavariables?
- hasLevelMVar : 1-bit -- does it contain level metavariables?
- hasLevelParam : 1-bit -- does it contain level parameters?
- looseBVarRange : 20-bits
Remark: this is mostly an internal datastructure used to implement Expr
,
most will never have to use it.
Instances For
Instances For
- name : Lake.Name
The unique free variable identifier. It is just a hierarchical name,
but we wrap it in FVarId
to make sure they don't get mixed up with MVarId
.
This is not the user-facing name for a free variable. This information is stored
in the local context (LocalContext
). The unique identifiers are generated using
a NameGenerator
.
Instances For
A set of unique free variable identifiers. This is a persistent data structure implemented using red-black trees.
Instances For
Instances For
A set of unique free variable identifiers implemented using hashtables. Hashtables are faster than red-black trees if they are used linearly. They are not persistent data-structures.
Instances For
A mapping from free variable identifiers to values of type α
.
This is a persistent data structure implemented using red-black trees.
Instances For
Instances For
Instances For
Instances For
Instances For
- bvar: Nat → Lean.Expr
The
bvar
constructor represents bound variables, i.e. occurrences of a variable in the expression where there is a variable binder above it (i.e. introduced by alam
,forallE
, orletE
).The
deBruijnIndex
parameter is the de-Bruijn index for the bound variable. See here for additional information on de-Bruijn indexes.For example, consider the expression
fun x : Nat => forall y : Nat, x = y
. Thex
andy
variables in the equality expression are constructed usingbvar
and bound to the binders introduced by the earlierlam
andforallE
constructors. Here is the correspondingExpr
representation for the same expression:.lam `x (.const `Nat []) (.forallE `y (.const `Nat []) (.app (.app (.app (.const `Eq [.succ .zero]) (.const `Nat [])) (.bvar 1)) (.bvar 0)) .default) .default
- fvar: Lean.FVarId → Lean.Expr
The
fvar
constructor represent free variables. These /free/ variable occurrences are not bound by an earlierlam
,forallE
, orletE
contructor and its binder exists in a local context only.Note that Lean uses the /locally nameless approach/. See here for additional details.
When "visiting" the body of a binding expression (i.e.
lam
,forallE
, orletE
), bound variables are converted into free variables using a unique identifier, and their user-facing name, type, value (forLetE
), and binder annotation are stored in theLocalContext
. - mvar: Lean.MVarId → Lean.Expr
Metavariables are used to represent "holes" in expressions, and goals in the tactic framework. Metavariable declarations are stored in the
MetavarContext
. Metavariables are used during elaboration, and are not allowed in the kernel, or in the code generator. - sort: Lean.Level → Lean.Expr
- const: Lake.Name → List Lean.Level → Lean.Expr
A (universe polymorphic) constant that has been defined earlier in the module or by another imported module. For example,
@Eq.{1}
is represented asExpr.const `Eq [.succ .zero]
, and@Array.map.{0, 0}
is represented asExpr.const `Array.map [.zero, .zero]
. - app: Lean.Expr → Lean.Expr → Lean.Expr
A function application.
For example, the natural number one, i.e.
Nat.succ Nat.zero
is represented asExpr.app (.const
Nat.succ []) (.const .zero [])` Note that multiple arguments are represented using partial application.For example, the two argument application
f x y
is represented asExpr.app (.app f x) y
. - lam: Lake.Name → Lean.Expr → Lean.Expr → Lean.BinderInfo → Lean.Expr
- forallE: Lake.Name → Lean.Expr → Lean.Expr → Lean.BinderInfo → Lean.Expr
A dependent arrow
(a : α) → β)
(aka forall-expression) whereβ
may dependent ona
. Note that this constructor is also used to represent non-dependent arrows whereβ
does not depend ona
.For example:
forall x : Prop, x ∧ x
:
Expr.forallE `x (.sort .zero) (.app (.app (.const `And []) (.bvar 0)) (.bvar 0)) .default
Expr.forallE `a (.const `Nat []) (.const `Bool []) .default
- letE: Lake.Name → Lean.Expr → Lean.Expr → Lean.Expr → Bool → Lean.Expr
Let-expressions.
IMPORTANT: The
nonDep
flag is for "local" use only. That is, a module should not "trust" its value for any purpose. In the intended use-case, the compiler will set this flag, and be responsible for maintaining it. Other modules may not preserve its value while applying transformations.Given an environment, a metavariable context, and a local context, we say a let-expression
let x : t := v; e
is non-dependent when it is equivalent to(fun x : t => e) v
. Here is an example of a dependent let-expressionlet n : Nat := 2; fun (a : Array Nat n) (b : Array Nat 2) => a = b
is type correct, but(fun (n : Nat) (a : Array Nat n) (b : Array Nat 2) => a = b) 2
is not.The let-expression
let x : Nat := 2; Nat.succ x
is represented asExpr.letE `x (.const `Nat []) (.lit (.natVal 2)) (.app (.const `Nat.succ []) (.bvar 0)) true
- lit: Lean.Literal → Lean.Expr
Natural number and string literal values.
They are not really needed, but provide a more compact representation in memory for these two kinds of literals, and are used to implement efficient reduction in the elaborator and kernel. The "raw" natural number
2
can be represented asExpr.lit (.natVal 2)
. Note that, it is definitionally equal to:Expr.app (.const `Nat.succ []) (.app (.const `Nat.succ []) (.const `Nat.zero []))
- mdata: Lean.MData → Lean.Expr → Lean.Expr
Metadata (aka annotations).
We use annotations to provide hints to the pretty-printer, store references to
Syntax
nodes, position information, and save information for elaboration procedures (e.g., we use theinaccessible
annotation during elaboration to markExpr
s that correspond to inaccessible patterns).Note that
Expr.mdata data e
is definitionally equal toe
. - proj: Lake.Name → Nat → Lean.Expr → Lean.Expr
Projection-expressions. They are redundant, but are used to create more compact terms, speedup reduction, and implement eta for structures. The type of
struct
must be an structure-like inductive type. That is, it has only one constructor, is not recursive, and it is not an inductive predicate. The kernel and elaborators check whether thetypeName
matches the type ofstruct
, and whether the (zero-based) index is valid (i.e., it is smaller than the numbef of constructor fields). When exporting Lean developments to other systems,proj
can be replaced withtypeName
.rec
applications.Example, given
a : Nat x Bool
,a.1
is represented as.proj `Prod 0 a
Lean expressions. This data structure is used in the kernel and elaborator. However, expressions sent to the kernel should not contain metavariables.
Remark: we use the E
suffix (short for Expr
) to avoid collision with keywords.
We considered using «...», but it is too inconvenient to use.
Instances For
The constructor name for the given expression. This is used for debugging purposes.
Instances For
Return true
if e
contains free variables.
This is a constant time operation.
Instances For
Return true
if e
contains expression metavariables.
This is a constant time operation.
Instances For
Return true
if e
contains universe (aka Level
) metavariables.
This is a constant time operation.
Instances For
Does the expression contain level (aka universe) or expression metavariables? This is a constant time operation.
Instances For
Return true if e
contains universe level parameters.
This is a constant time operation.
Instances For
Return the approximated depth of an expression. This information is used to compute
the expression hash code, and speedup comparisons.
This is a constant time operation. We say it is approximate because it maxes out at 255
.
Instances For
The range of de-Bruijn variables that are loose.
That is, bvars that are not bound by a binder.
For example, bvar i
has range i + 1
and
an expression with no loose bvars has range 0
.
Instances For
Return the binder information if e
is a lambda or forall expression, and .default
otherwise.
Instances For
Export functions.
Instances For
Instances For
Instances For
Instances For
Return the type of a literal value.
Instances For
.fvar fvarId
is now the preferred form.
This function is seldom used, free variables are often automatically created using the
telescope functions (e.g., forallTelescope
and lambdaTelescope
) at MetaM
.
Instances For
.mvar mvarId
is now the preferred form.
This function is seldom used, metavariables are often created using functions such
as mkFresheExprMVar
at MetaM
.
Instances For
.mdata m e
is now the preferred form.
Instances For
.lam x t b bi
is now the preferred form.
Instances For
.forallE x t b bi
is now the preferred form.
Instances For
Return a natural number literal used in the frontend. It is a OfNat.ofNat
application.
Recall that all theorems and definitions containing numeric literals are encoded using
OfNat.ofNat
applications in the frontend.
Instances For
Instances For
Instances For
Instances For
Instances For
mkAppRange f i j #[a_1, ..., a_i, ..., a_j, ... ]
==> the expression f a_i ... a_{j-1}
Instances For
A total order for expressions. We say it is quick because it first compares the hashcodes.
A total order for expressions that takes the structure into account (e.g., variable names).
Return true iff a
and b
are alpha equivalent.
Binder annotations are ignored.
Return true iff a
and b
are equal.
Binder names and annotations are taking into account.
Return true
if the given expression is a .sort ..
Instances For
Return true
if the given expression is of the form .sort (.succ ..)
.
Instances For
Return true
if the given expression is of the form .sort (.succ .zero)
.
Instances For
Return true
if the given expression is a .sort .zero
Instances For
Return true
if the given expression is a bound variable.
Instances For
Return true
if the given expression is a metavariable.
Instances For
Return true
if the given expression is a free variable.
Instances For
Return true
if the given expression is an application.
Instances For
Return true
if the given expression is a projection .proj ..
Instances For
Return true
if the given expression is a constant.
Instances For
Return true
if the given expression is a forall-expression aka (dependent) arrow.
Instances For
Return true
if the given expression is a lambda abstraction aka anonymous function.
Instances For
Return true
if the given expression is a forall or lambda expression.
Instances For
Return true
if the given expression is a let-expression.
Instances For
Return true
if the given expression is a metadata.
Instances For
Return true
if the given expression is a literal value.
Instances For
Return the "body" of a forall expression.
Example: let e
be the representation for forall (p : Prop) (q : Prop), p ∧ q
, then
getForallBody e
returns .app (.app (.const `And []) (.bvar 1)) (.bvar 0)
Equations
- Lean.Expr.getForallBody (Lean.Expr.forallE binderName binderType body binderInfo) = Lean.Expr.getForallBody body
- Lean.Expr.getForallBody x = x
Instances For
Equations
- Lean.Expr.getForallBodyMaxDepth (Nat.succ n) (Lean.Expr.forallE binderName binderType b binderInfo) = Lean.Expr.getForallBodyMaxDepth n b
- Lean.Expr.getForallBodyMaxDepth 0 x = x
- Lean.Expr.getForallBodyMaxDepth x x = x
Instances For
Given a sequence of nested foralls (a₁ : α₁) → ... → (aₙ : αₙ) → _
,
returns the names [a₁, ... aₙ]
.
Equations
- Lean.Expr.getForallBinderNames (Lean.Expr.forallE binderName binderType body binderInfo) = binderName :: Lean.Expr.getForallBinderNames body
- Lean.Expr.getForallBinderNames x = []
Instances For
If the given expression is a sequence of
function applications f a₁ .. aₙ
, return f
.
Otherwise return the input expression.
Equations
- Lean.Expr.getAppFn (Lean.Expr.app fn arg) = Lean.Expr.getAppFn fn
- Lean.Expr.getAppFn x = x
Instances For
Counts the number n
of arguments for an expression f a₁ .. aₙ
.
Instances For
Given f a₁ a₂ ... aₙ
, returns #[a₁, ..., aₙ]
Instances For
Equations
- Lean.Expr.withAppAux k (Lean.Expr.app f a) x x = Lean.Expr.withAppAux k f (Array.set! x x a) (x - 1)
- Lean.Expr.withAppAux k x x x = k x x
Instances For
Equations
- Lean.Expr.getRevArgD (Lean.Expr.app fn a) 0 x = a
- Lean.Expr.getRevArgD (Lean.Expr.app f arg) (Nat.succ i) x = Lean.Expr.getRevArgD f i x
- Lean.Expr.getRevArgD x x x = x
Instances For
Equations
- Lean.Expr.getRevArg! (Lean.Expr.app fn a) 0 = a
- Lean.Expr.getRevArg! (Lean.Expr.app f arg) (Nat.succ i) = Lean.Expr.getRevArg! f i
- Lean.Expr.getRevArg! x x = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.getRevArg!" 972 20 "invalid index"
Instances For
Given f a₀ a₁ ... aₙ
, returns the i
th argument or panics if out of bounds.
Instances For
Given f a₀ a₁ ... aₙ
, returns the i
th argument or returns v₀
if out of bounds.
Instances For
Given f a₀ a₁ ... aₙ
, returns true if f
is a constant with name n
.
Instances For
Given f a₁ ... aᵢ
, returns true if f
is a constant
with name n
and has the correct number of arguments.
Equations
- Lean.Expr.isAppOfArity (Lean.Expr.const c us) x 0 = (c == x)
- Lean.Expr.isAppOfArity (Lean.Expr.app f arg) x (Nat.succ a) = Lean.Expr.isAppOfArity f x a
- Lean.Expr.isAppOfArity x x x = false
Instances For
Similar to isAppOfArity
but skips Expr.mdata
.
Equations
- Lean.Expr.isAppOfArity' (Lean.Expr.mdata data b) x x = Lean.Expr.isAppOfArity' b x x
- Lean.Expr.isAppOfArity' (Lean.Expr.const c us) x 0 = (c == x)
- Lean.Expr.isAppOfArity' (Lean.Expr.app f arg) x (Nat.succ a) = Lean.Expr.isAppOfArity' f x a
- Lean.Expr.isAppOfArity' x x x = false
Instances For
Equations
- Lean.Expr.appFn!' (Lean.Expr.mdata data b) = Lean.Expr.appFn!' b
- Lean.Expr.appFn!' (Lean.Expr.app f arg) = f
- Lean.Expr.appFn!' x = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appFn!'" 1015 17 "application expected"
Instances For
Equations
- Lean.Expr.appArg!' (Lean.Expr.mdata data b) = Lean.Expr.appArg!' b
- Lean.Expr.appArg!' (Lean.Expr.app f arg) = arg
- Lean.Expr.appArg!' x = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appArg!'" 1020 17 "application expected"
Instances For
Equations
- Lean.Expr.consumeMData (Lean.Expr.mdata data expr) = Lean.Expr.consumeMData expr
- Lean.Expr.consumeMData x = x
Instances For
Return true
if e
is a non-dependent arrow.
Remark: the following function assumes e
does not have loose bound variables.
Instances For
Return true if e
contains the loose bound variable bvarIdx
in an explicit parameter, or in the range if tryRange == true
.
Equations
- One or more equations did not get rendered due to their size.
- Lean.Expr.hasLooseBVarInExplicitDomain x x x = (x && Lean.Expr.hasLooseBVar x x)
Instances For
inferImplicit e numParams considerRange
updates the first numParams
parameter binder annotations of the e
forall type.
It marks any parameter with an explicit binder annotation if there is another explicit arguments that depends on it or
the resulting type if considerRange == true
.
Remark: we use this function to infer the bind annotations of inductive datatype constructors, and structure projections.
When the {}
annotation is used in these commands, we set considerRange == false
.
Instances For
Similar to instantiate
, but consider only the variables xs
in the range [beginIdx, endIdx)
.
Function panics if beginIdx <= endIdx <= xs.size
does not hold.
Similar to instantiateRev
, but consider only the variables xs
in the range [beginIdx, endIdx)
.
Function panics if beginIdx <= endIdx <= xs.size
does not hold.
Replace occurrences of the free variable fvarId
in e
with v
Instances For
Returns true when the expression does not have any sub-expressions.
Instances For
mkAppRevRange f b e args == mkAppRev f (revArgs.extract b e)
Instances For
If f
is a lambda expression, than "beta-reduce" it using revArgs
.
This function is often used with getAppRev
or withAppRev
.
Examples:
betaRev (fun x y => t x y) #[]
==>fun x y => t x y
betaRev (fun x y => t x y) #[a]
==>fun y => t a y
betaRev (fun x y => t x y) #[a, b]
==>t b a
betaRev (fun x y => t x y) #[a, b, c, d]
==>t d c b a
Supposet
is(fun x y => t x y) a b c d
, thenargs := t.getAppRev
is#[d, c, b, a]
, andbetaRev (fun x y => t x y) #[d, c, b, a]
ist a b c d
.
If useZeta
is true, the function also performs zeta-reduction (reduction of let binders) to create further
opportunities for beta reduction.
Instances For
Return true if the given expression is the function of an expression that is target for (head) beta reduction.
If useZeta = true
, then let
-expressions are visited. That is, it assumes
that zeta-reduction (aka let-expansion) is going to be used.
See isHeadBetaTarget
.
Equations
- Lean.Expr.isHeadBetaTargetFn useZeta (Lean.Expr.lam binderName binderType b binderInfo) = true
- Lean.Expr.isHeadBetaTargetFn useZeta (Lean.Expr.letE declName type v b nonDep) = (useZeta && Lean.Expr.isHeadBetaTargetFn useZeta b)
- Lean.Expr.isHeadBetaTargetFn useZeta (Lean.Expr.mdata k b) = Lean.Expr.isHeadBetaTargetFn useZeta b
- Lean.Expr.isHeadBetaTargetFn useZeta x = false
Instances For
Return true if the given expression is a target for (head) beta reduction.
If useZeta = true
, then let
-expressions are visited. That is, it assumes
that zeta-reduction (aka let-expansion) is going to be used.
Instances For
If e
is of the form (fun x₁ ... xₙ => f x₁ ... xₙ)
and f
does not contain x₁
, ..., xₙ
,
then return some f
. Otherwise, return none
.
It assumes e
does not have loose bound variables.
Remark: ₙ
may be 0
Instances For
Similar to etaExpanded?
, but only succeeds if ₙ ≥ 1
.
Instances For
Return true
if e
is of the form semiOutParam _
Instances For
Return true
if e
is of the form optParam _ _
Instances For
Return true
if e
is of the form autoParam _ _
Instances For
Remove outParam
, optParam
, and autoParam
applications/annotations from e
.
Note that it does not remove nested annotations.
Examples:
- Given
e
of the formoutParam (optParam Nat b)
,consumeTypeAnnotations e = b
. - Given
e
of the formNat → outParam (optParam Nat b)
,consumeTypeAnnotations e = e
.
Remove metadata annotations and outParam
, optParam
, and autoParam
applications/annotations from e
.
Note that it does not remove nested annotations.
Examples:
- Given
e
of the formoutParam (optParam Nat b)
,cleanupAnnotations e = b
. - Given
e
of the formNat → outParam (optParam Nat b)
,cleanupAnnotations e = e
.
Return true iff e
contains a free variable which statisfies p
.
Instances For
Instances For
Return true
if e
contains the given free variable.
Instances For
The update functions try to avoid allocating new values using pointer equality.
Note that if the update*!
functions are used under a match-expression,
the compiler will eliminate the double-match.
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Equations
- Lean.Expr.updateFn (Lean.Expr.app f a) x = Lean.Expr.updateApp! (Lean.Expr.app f a) (Lean.Expr.updateFn f x) a
- Lean.Expr.updateFn x x = x
Instances For
Eta reduction. If e
is of the form (fun x => f x)
, then return f
.
Annotate e
with the given option.
The information is stored using metadata around e
.
Instances For
Annotate e
with pp.explicit := flag
The delaborator uses pp
options.
Instances For
Annotate e
with pp.universes := flag
The delaborator uses pp
options.
Instances For
If e
is an application f a_1 ... a_n
annotate f
, a_1
... a_n
with pp.explicit := false
,
and annotate e
with pp.explicit := true
.
Instances For
Similar for setAppPPExplicit
, but only annotate children with pp.explicit := false
if
e
does not contain metavariables.
Instances For
Annotate e
with the given annotation name kind
.
It uses metadata to store the annotation.
Instances For
Return some e'
if e = mkAnnotation kind e'
Instances For
Annotate e
with the let_fun
annotation. This annotation is used as hint for the delaborator.
If e
is of the form (fun x : t => b) v
, then mkLetFunAnnotation e
is delaborated at
let_fun x : t := v; b
Instances For
Return some e'
if e = mkLetFunAnnotation e'
Instances For
Return true if e = mkLetFunAnnotation e'
, and e'
is of the form (fun x : t => b) v
Instances For
Auxiliary annotation used to mark terms marked with the "inaccessible" annotation .(t)
and
_
in patterns.
Instances For
Return some e'
if e = mkInaccessible e'
.
Instances For
During elaboration expressions corresponding to pattern matching terms
are annotated with Syntax
objects. This function returns some (stx, p')
if
p
is the pattern p'
annotated with stx
Instances For
Annotate the pattern p
with stx
. This is an auxiliary annotation
for producing better hover information.
Instances For
Return some p
if e
is an annotated pattern (inaccessible?
or patternWithRef?
)
Instances For
Annotate e
with the LHS annotation. The delaborator displays
expressions of the form lhs = rhs
as lhs
when they have this annotation.
This is used to implement the infoview for the conv
mode.
This version of mkLHSGoal
does not check that the argument is an equality.
Instances For
Return some lhs
if e = mkLHSGoal e'
, where e'
is of the form lhs = rhs
.
Instances For
Polymorphic operation for generating unique/fresh free variable identifiers.
It is available in any monad m
that implements the inferface MonadNameGenerator
.
Instances For
Polymorphic operation for generating unique/fresh metavariable identifiers.
It is available in any monad m
that implements the inferface MonadNameGenerator
.
Instances For
Polymorphic operation for generating unique/fresh universe metavariable identifiers.
It is available in any monad m
that implements the inferface MonadNameGenerator
.