- 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_declis used for_match,_fun_match,_let_matchand 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
bvarconstructor 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
deBruijnIndexparameter 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. Thexandyvariables in the equality expression are constructed usingbvarand bound to the binders introduced by the earlierlamandforallEconstructors. Here is the correspondingExprrepresentation 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
fvarconstructor represent free variables. These /free/ variable occurrences are not bound by an earlierlam,forallE, orletEcontructor 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.zerois represented asExpr.app (.constNat.succ []) (.const .zero [])` Note that multiple arguments are represented using partial application.For example, the two argument application
f x yis 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)) .defaultExpr.forallE `a (.const `Nat []) (.const `Bool []) .default - letE: Lake.Name → Lean.Expr → Lean.Expr → Lean.Expr → Bool → Lean.Expr
Let-expressions.
IMPORTANT: The
nonDepflag 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; eis 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 = bis type correct, but(fun (n : Nat) (a : Array Nat n) (b : Array Nat 2) => a = b) 2is not.The let-expression
let x : Nat := 2; Nat.succ xis 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
2can 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
Syntaxnodes, position information, and save information for elaboration procedures (e.g., we use theinaccessibleannotation during elaboration to markExprs that correspond to inaccessible patterns).Note that
Expr.mdata data eis 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
structmust 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 thetypeNamematches 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,projcan be replaced withtypeName.recapplications.Example, given
a : Nat x Bool,a.1is 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 ith argument or panics if out of bounds.
Instances For
Given f a₀ a₁ ... aₙ, returns the ith 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 ybetaRev (fun x y => t x y) #[a]==>fun y => t a ybetaRev (fun x y => t x y) #[a, b]==>t b abetaRev (fun x y => t x y) #[a, b, c, d]==>t d c b aSupposetis(fun x y => t x y) a b c d, thenargs := t.getAppRevis#[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
eof the formoutParam (optParam Nat b),consumeTypeAnnotations e = b. - Given
eof 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
eof the formoutParam (optParam Nat b),cleanupAnnotations e = b. - Given
eof 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.