- natVal: Nat → Lean.Literal
Natural number literal
- strVal: String → Lean.Literal
String literal
Literal values for Expr
.
Instances For
Equations
- Lean.instInhabitedLiteral = { default := Lean.Literal.natVal default }
Equations
- Lean.instBEqLiteral = { beq := Lean.beqLiteral✝ }
Equations
- Lean.instReprLiteral = { reprPrec := Lean.reprLiteral✝ }
Equations
- Lean.Literal.hash _fun_discr = match _fun_discr with | Lean.Literal.natVal v => hash v | Lean.Literal.strVal v => hash v
Equations
- Lean.instHashableLiteral = { hash := Lean.Literal.hash }
Total order on Expr
literal values.
Natural number values are smaller than string literal values.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.instLTLiteral = { lt := fun a b => Lean.Literal.lt a b = true }
Equations
- 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 α]
- auxDecl: Lean.BinderInfo
Auxiliary declarations used by Lean when elaborating recursive declarations. When defining a function such as
def f : Nat → Nat | 0 => 1 | x+1 => (x+1)*f x
Lean adds a local declaration
f : Nat → Nat
to the local context (LocalContext
) withBinderInfo
set toauxDecl
. This local declaration is later removed by the termination checker.
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
Equations
- Lean.instInhabitedBinderInfo = { default := Lean.BinderInfo.default }
Equations
- Lean.instBEqBinderInfo = { beq := Lean.beqBinderInfo✝ }
Equations
- Lean.instReprBinderInfo = { reprPrec := Lean.reprBinderInfo✝ }
Equations
- One or more equations did not get rendered due to their size.
Return true
if the given BinderInfo
does not correspond to an implicit binder annotation
(i.e., implicit
, strictImplicit
, or instImplicit
).
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.instHashableBinderInfo = { hash := Lean.BinderInfo.hash }
Return true
if the given BinderInfo
is an instance implicit annotation (e.g., [Decidable α]
)
Equations
- Lean.BinderInfo.isInstImplicit _fun_discr = match _fun_discr with | Lean.BinderInfo.instImplicit => true | x => false
Return true
if the given BinderInfo
is a regular implicit annotation (e.g., {α : Type u}
)
Equations
- Lean.BinderInfo.isImplicit _fun_discr = match _fun_discr with | Lean.BinderInfo.implicit => true | x => false
Return true
if the given BinderInfo
is a strict implicit annotation (e.g., {{α : Type u}}
)
Equations
- Lean.BinderInfo.isStrictImplicit _fun_discr = match _fun_discr with | Lean.BinderInfo.strictImplicit => true | x => false
Equations
- Lean.BinderInfo.isAuxDecl _fun_discr = match _fun_discr with | Lean.BinderInfo.auxDecl => true | x => false
Expression metadata. Used with the Expr.mdata
constructor.
Equations
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.
Equations
Equations
Equations
Equations
- Lean.instBEqData_1 = { beq := fun a b => a == b }
Equations
- Lean.Expr.Data.approxDepth c = UInt64.toUInt8 (UInt64.land (UInt64.shiftRight c 32) 255)
Equations
Equations
- Lean.Expr.Data.hasFVar c = (UInt64.land (UInt64.shiftRight c 40) 1 == 1)
Equations
- Lean.Expr.Data.hasExprMVar c = (UInt64.land (UInt64.shiftRight c 41) 1 == 1)
Equations
- Lean.Expr.Data.hasLevelMVar c = (UInt64.land (UInt64.shiftRight c 42) 1 == 1)
Equations
- Lean.Expr.Data.hasLevelParam c = (UInt64.land (UInt64.shiftRight c 43) 1 == 1)
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.
Optimized version of Expr.mkData
for applications.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Expr.mkDataForBinder h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam = Lean.Expr.mkData h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam
Equations
- Lean.Expr.mkDataForLet h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam = Lean.Expr.mkData h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam
Equations
- One or more equations did not get rendered due to their size.
- name : Lean.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
Equations
- Lean.instInhabitedFVarId = { default := { name := default } }
Equations
- Lean.instBEqFVarId = { beq := Lean.beqFVarId✝ }
Equations
- Lean.instHashableFVarId = { hash := Lean.hashFVarId✝ }
Equations
- Lean.instReprFVarId = { reprPrec := fun n p => reprPrec n.name p }
A set of unique free variable identifiers. This is a persistent data structure implemented using red-black trees.
Equations
- Lean.FVarIdSet = Lean.RBTree Lean.FVarId fun a a_1 => Lean.Name.quickCmp a.name a_1.name
Equations
- Lean.instForInFVarIdSetFVarId = inferInstanceAs (ForIn m (Lean.RBTree Lean.FVarId fun a a_1 => Lean.Name.quickCmp a.name a_1.name) Lean.FVarId)
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.
Equations
A mapping from free variable identifiers to values of type α
.
This is a persistent data structure implemented using red-black trees.
Equations
- Lean.FVarIdMap α = Lean.RBMap Lean.FVarId α fun a a_1 => Lean.Name.quickCmp a.name a_1.name
Equations
- Lean.instEmptyCollectionFVarIdMap = inferInstanceAs (EmptyCollection (Lean.RBMap Lean.FVarId α fun a a_1 => Lean.Name.quickCmp a.name a_1.name))
Equations
- Lean.instInhabitedMVarId = { default := { name := default } }
Equations
- Lean.instBEqMVarId = { beq := Lean.beqMVarId✝ }
Equations
- Lean.instHashableMVarId = { hash := Lean.hashMVarId✝ }
Equations
- Lean.instReprMVarId = { reprPrec := Lean.reprMVarId✝ }
Equations
- Lean.instReprMVarId_1 = { reprPrec := fun n p => reprPrec n.name p }
Equations
- Lean.MVarIdSet = Lean.RBTree Lean.MVarId fun a a_1 => Lean.Name.quickCmp a.name a_1.name
Equations
- Lean.instForInMVarIdSetMVarId = inferInstanceAs (ForIn m (Lean.RBTree Lean.MVarId fun a a_1 => Lean.Name.quickCmp a.name a_1.name) Lean.MVarId)
Equations
- Lean.MVarIdMap α = Lean.RBMap Lean.MVarId α fun a a_1 => Lean.Name.quickCmp a.name a_1.name
Equations
- Lean.instEmptyCollectionMVarIdMap = inferInstanceAs (EmptyCollection (Lean.RBMap Lean.MVarId α fun a a_1 => Lean.Name.quickCmp a.name a_1.name))
Equations
- Lean.instForInMVarIdMapProdMVarId = inferInstanceAs (ForIn m (Lean.RBMap Lean.MVarId α fun a a_1 => Lean.Name.quickCmp a.name a_1.name) (Lean.MVarId × α))
- 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
Used for
Type u
,Sort u
, andProp
:Prop
is represented as.sort .zero
,Sort u
as.sort (.param `u)
, andType u
as.sort (.succ (.param `u))
- const: Lean.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: Lean.Name → Lean.Expr → Lean.Expr → Lean.BinderInfo → Lean.Expr
A lambda abstraction (aka anonymous functions). It introduces a new binder for variable
x
in scope for the lambda body.For example, the expression
fun x : Nat => x
is represented asExpr.lam `x (.const `Nat []) (.bvar 0) .default
- forallE: Lean.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: Lean.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)) (.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: Lean.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
Equations
- Lean.instInhabitedExpr = { default := Lean.Expr.bvar default }
Equations
- Lean.instReprExpr = { reprPrec := Lean.reprExpr✝ }
The constructor name for the given expression. This is used for debugging purposes.
Equations
- One or more equations did not get rendered due to their size.
Equations
Equations
- Lean.Expr.instHashableExpr = { hash := Lean.Expr.hash }
Return true
if e
contains free variables.
This is a constant time operation.
Equations
Return true
if e
contains expression metavariables.
This is a constant time operation.
Equations
Return true
if e
contains universe (aka Level
) metavariables.
This is a constant time operation.
Equations
Does the expression contain level (aka universe) or expression metavariables? This is a constant time operation.
Equations
- Lean.Expr.hasMVar e = let d := Lean.Expr.data e; Lean.Expr.Data.hasExprMVar d || Lean.Expr.Data.hasLevelMVar d
Return true if e
contains universe level parameters.
This is a constant time operation.
Equations
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
.
Equations
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
.
Equations
Return the binder information if e
is a lambda or forall expression, and .default
otherwise.
Equations
- Lean.Expr.binderInfo e = match e with | Lean.Expr.forallE binderName binderType body bi => bi | Lean.Expr.lam binderName binderType body bi => bi | x => Lean.BinderInfo.default
Export functions.
Equations
- Lean.Expr.hashEx = hash
Equations
Equations
Equations
Equations
mkConst declName us
return .const declName us
.
Equations
- Lean.mkConst declName us = Lean.Expr.const declName us
Return the type of a literal value.
Equations
- One or more equations did not get rendered due to their size.
Equations
.bvar idx
is now the preferred form.
Equations
- Lean.mkBVar idx = Lean.Expr.bvar idx
.sort u
is now the preferred form.
Equations
.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
.
Equations
- Lean.mkFVar fvarId = Lean.Expr.fvar fvarId
.mvar mvarId
is now the preferred form.
This function is seldom used, metavariables are often created using functions such
as mkFresheExprMVar
at MetaM
.
Equations
- Lean.mkMVar mvarId = Lean.Expr.mvar mvarId
.mdata m e
is now the preferred form.
Equations
- Lean.mkMData m e = Lean.Expr.mdata m e
.proj structName idx struct
is now the preferred form.
Equations
- Lean.mkProj structName idx struct = Lean.Expr.proj structName idx struct
.app f a
is now the preferred form.
Equations
- Lean.mkApp f a = Lean.Expr.app f a
.lam x t b bi
is now the preferred form.
Equations
- Lean.mkLambda x bi t b = Lean.Expr.lam x t b bi
.forallE x t b bi
is now the preferred form.
Equations
- Lean.mkForall x bi t b = Lean.Expr.forallE x t b bi
Return Unit -> type
. Do not confuse with Thunk type
Equations
- Lean.mkSimpleThunkType type = Lean.mkForall Lean.Name.anonymous Lean.BinderInfo.default (Lean.mkConst (Lean.Name.mkStr1 "Unit")) type
Return fun (_ : Unit), e
Equations
- Lean.mkSimpleThunk type = Lean.mkLambda (Lean.Name.mkStr1 "_") Lean.BinderInfo.default (Lean.mkConst (Lean.Name.mkStr1 "Unit")) type
.letE x t v b nonDep
is now the preferred form.
Equations
- Lean.mkLet x t v b nonDep = Lean.Expr.letE x t v b nonDep
Equations
- Lean.mkAppB f a b = Lean.mkApp (Lean.mkApp f a) b
Equations
- Lean.mkApp2 f a b = Lean.mkAppB f a b
Equations
- Lean.mkApp3 f a b c = Lean.mkApp (Lean.mkAppB f a b) c
Equations
- Lean.mkApp4 f a b c d = Lean.mkAppB (Lean.mkAppB f a b) c d
Equations
- Lean.mkApp5 f a b c d e = Lean.mkApp (Lean.mkApp4 f a b c d) e
Equations
- Lean.mkApp6 f a b c d e₁ e₂ = Lean.mkAppB (Lean.mkApp4 f a b c d) e₁ e₂
Equations
- Lean.mkApp7 f a b c d e₁ e₂ e₃ = Lean.mkApp3 (Lean.mkApp4 f a b c d) e₁ e₂ e₃
Equations
- Lean.mkApp8 f a b c d e₁ e₂ e₃ e₄ = Lean.mkApp4 (Lean.mkApp4 f a b c d) e₁ e₂ e₃ e₄
Equations
- Lean.mkApp9 f a b c d e₁ e₂ e₃ e₄ e₅ = Lean.mkApp5 (Lean.mkApp4 f a b c d) e₁ e₂ e₃ e₄ e₅
Equations
- Lean.mkApp10 f a b c d e₁ e₂ e₃ e₄ e₅ e₆ = Lean.mkApp6 (Lean.mkApp4 f a b c d) e₁ e₂ e₃ e₄ e₅ e₆
.lit l
is now the preferred form.
Equations
- Lean.mkLit l = Lean.Expr.lit l
Return the "raw" natural number .lit (.natVal n)
.
This is not the default representation used by the Lean frontend.
See mkNatLit
.
Equations
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.
Equations
- One or more equations did not get rendered due to their size.
Return the string literal .lit (.strVal s)
Equations
Equations
Equations
Equations
Equations
Equations
- Lean.mkConstEx c lvls = Lean.mkConst c lvls
Equations
Equations
- Lean.mkLambdaEx n d b bi = Lean.mkLambda n bi d b
Equations
- Lean.mkForallEx n d b bi = Lean.mkForall n bi d b
Equations
- Lean.mkLetEx n t v b = Lean.mkLet n t v b
Equations
Equations
Equations
mkAppN f #[a₀, ..., aₙ]
==> f a₀ a₁ .. aₙ
Equations
- Lean.mkAppN f args = Array.foldl Lean.mkApp f args 0 (Array.size args)
mkAppRange f i j #[a_1, ..., a_i, ..., a_j, ... ]
==> the expression f a_i ... a_{j-1}
Equations
- Lean.mkAppRange f i j args = Lean.mkAppRangeAux j args i f
Same as mkApp f args
but reversing args
.
Equations
- Lean.mkAppRev fn revArgs = Array.foldr (fun a r => Lean.mkApp r a) fn revArgs (Array.size revArgs)
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.
Equations
- Lean.Expr.instBEqExpr = { beq := Lean.Expr.eqv }
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 ..
Equations
- Lean.Expr.isSort _fun_discr = match _fun_discr with | Lean.Expr.sort u => true | x => false
Return true
if the given expression is of the form .sort (.succ ..)
.
Equations
- Lean.Expr.isType _fun_discr = match _fun_discr with | Lean.Expr.sort (Lean.Level.succ a) => true | x => false
Return true
if the given expression is of the form .sort (.succ .zero)
.
Equations
- Lean.Expr.isType0 _fun_discr = match _fun_discr with | Lean.Expr.sort (Lean.Level.succ Lean.Level.zero) => true | x => false
Return true
if the given expression is a .sort .zero
Equations
- Lean.Expr.isProp _fun_discr = match _fun_discr with | Lean.Expr.sort Lean.Level.zero => true | x => false
Return true
if the given expression is a bound variable.
Equations
- Lean.Expr.isBVar _fun_discr = match _fun_discr with | Lean.Expr.bvar deBruijnIndex => true | x => false
Return true
if the given expression is a metavariable.
Equations
- Lean.Expr.isMVar _fun_discr = match _fun_discr with | Lean.Expr.mvar mvarId => true | x => false
Return true
if the given expression is a free variable.
Equations
- Lean.Expr.isFVar _fun_discr = match _fun_discr with | Lean.Expr.fvar fvarId => true | x => false
Return true
if the given expression is an application.
Equations
- Lean.Expr.isApp _fun_discr = match _fun_discr with | Lean.Expr.app fn arg => true | x => false
Return true
if the given expression is a projection .proj ..
Equations
- Lean.Expr.isProj _fun_discr = match _fun_discr with | Lean.Expr.proj typeName idx struct => true | x => false
Return true
if the given expression is a constant.
Equations
- Lean.Expr.isConst _fun_discr = match _fun_discr with | Lean.Expr.const declName us => true | x => false
Return true
if the given expression is a constant of the give name.
Examples:
Equations
- Lean.Expr.isConstOf _fun_discr _fun_discr = match _fun_discr, _fun_discr with | Lean.Expr.const n us, m => n == m | x, x_1 => false
Return true
if the given expression is a free variable with the given id.
Examples:
isFVarOf (.fvar id) id
istrue
isFVarOf (.fvar id) id'
isfalse
isFVarOf (.sort levelZero) id
isfalse
Equations
- Lean.Expr.isFVarOf _fun_discr _fun_discr = match _fun_discr, _fun_discr with | Lean.Expr.fvar fvarId, fvarId' => fvarId == fvarId' | x, x_1 => false
Return true
if the given expression is a forall-expression aka (dependent) arrow.
Equations
- Lean.Expr.isForall _fun_discr = match _fun_discr with | Lean.Expr.forallE binderName binderType body binderInfo => true | x => false
Return true
if the given expression is a lambda abstraction aka anonymous function.
Equations
- Lean.Expr.isLambda _fun_discr = match _fun_discr with | Lean.Expr.lam binderName binderType body binderInfo => true | x => false
Return true
if the given expression is a forall or lambda expression.
Equations
- One or more equations did not get rendered due to their size.
Return true
if the given expression is a let-expression.
Equations
- Lean.Expr.isLet _fun_discr = match _fun_discr with | Lean.Expr.letE declName type value body nonDep => true | x => false
Return true
if the given expression is a metadata.
Equations
- Lean.Expr.isMData _fun_discr = match _fun_discr with | Lean.Expr.mdata data expr => true | x => false
Return true
if the given expression is a literal value.
Equations
- Lean.Expr.isLit _fun_discr = match _fun_discr with | Lean.Expr.lit a => true | x => false
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 _fun_discr = _fun_discr
Equations
- Lean.Expr.getForallBodyMaxDepth (Nat.succ n) (Lean.Expr.forallE binderName binderType b binderInfo) = Lean.Expr.getForallBodyMaxDepth n b
- Lean.Expr.getForallBodyMaxDepth 0 _fun_discr = _fun_discr
- Lean.Expr.getForallBodyMaxDepth _fun_discr _fun_discr = _fun_discr
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 _fun_discr = []
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 _fun_discr = _fun_discr
Counts the number n
of arguments for an expression f a₁ .. aₙ
.
Equations
Given f a₁ a₂ ... aₙ
, returns #[a₁, ..., aₙ]
Equations
- Lean.Expr.getAppArgs e = let dummy := Lean.mkSort Lean.levelZero; let nargs := Lean.Expr.getAppNumArgs e; Lean.Expr.getAppArgsAux e (mkArray nargs dummy) (nargs - 1)
Equations
- Lean.Expr.withAppAux k (Lean.Expr.app f a) _fun_discr _fun_discr = Lean.Expr.withAppAux k f (Array.set! _fun_discr _fun_discr a) (_fun_discr - 1)
- Lean.Expr.withAppAux k _fun_discr _fun_discr _fun_discr = k _fun_discr _fun_discr
Given e = f a₁ a₂ ... aₙ
, returns k f #[a₁, ..., aₙ]
.
Equations
- Lean.Expr.withApp e k = let dummy := Lean.mkSort Lean.levelZero; let nargs := Lean.Expr.getAppNumArgs e; Lean.Expr.withAppAux k e (mkArray nargs dummy) (nargs - 1)
Given e = fn a₁ ... aₙ
, runs f
on fn
and each of the arguments aᵢ
and
makes a new function application with the results.
Equations
- Lean.Expr.traverseApp f e = Lean.Expr.withApp e fun fn args => Seq.seq (Lean.mkAppN <$> f fn) fun x => Array.mapM f args
Equations
- Lean.Expr.getRevArgD (Lean.Expr.app fn a) 0 _fun_discr = a
- Lean.Expr.getRevArgD (Lean.Expr.app f arg) (Nat.succ i) _fun_discr = Lean.Expr.getRevArgD f i _fun_discr
- Lean.Expr.getRevArgD _fun_discr _fun_discr _fun_discr = _fun_discr
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! _fun_discr _fun_discr = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.getRevArg!" 977 20 "invalid index"
Given f a₀ a₁ ... aₙ
, returns the i
th argument or panics if out of bounds.
Equations
- Lean.Expr.getArg! e i n = Lean.Expr.getRevArg! e (n - i - 1)
Given f a₀ a₁ ... aₙ
, returns the i
th argument or returns v₀
if out of bounds.
Equations
- Lean.Expr.getArgD e i v₀ n = Lean.Expr.getRevArgD e (n - i - 1) v₀
Given f a₀ a₁ ... aₙ
, returns true if f
is a constant with name n
.
Equations
- Lean.Expr.isAppOf e n = match Lean.Expr.getAppFn e with | Lean.Expr.const c us => c == n | x => false
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) _fun_discr 0 = (c == _fun_discr)
- Lean.Expr.isAppOfArity (Lean.Expr.app f arg) _fun_discr (Nat.succ a) = Lean.Expr.isAppOfArity f _fun_discr a
- Lean.Expr.isAppOfArity _fun_discr _fun_discr _fun_discr = false
Similar to isAppOfArity
but skips Expr.mdata
.
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.
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!' _fun_discr = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appFn!'" 1020 17 "application expected"
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!' _fun_discr = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appArg!'" 1025 17 "application expected"
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.
Equations
- Lean.Expr.isNatLit _fun_discr = match _fun_discr with | Lean.Expr.lit (Lean.Literal.natVal val) => true | x => false
Equations
- Lean.Expr.natLit? _fun_discr = match _fun_discr with | Lean.Expr.lit (Lean.Literal.natVal v) => some v | x => none
Equations
- Lean.Expr.isStringLit _fun_discr = match _fun_discr with | Lean.Expr.lit (Lean.Literal.strVal val) => true | x => false
Equations
- Lean.Expr.isCharLit e = (Lean.Expr.isAppOfArity e (Lean.Name.mkStr2 "Char" "ofNat") 1 && Lean.Expr.isNatLit (Lean.Expr.appArg! e))
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Expr.constName? _fun_discr = match _fun_discr with | Lean.Expr.const n us => some n | x => none
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.
Equations
- Lean.Expr.fvarId! _fun_discr = match _fun_discr with | Lean.Expr.fvar n => n | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.fvarId!" 1068 14 "fvar expected"
Equations
- Lean.Expr.mvarId! _fun_discr = match _fun_discr with | Lean.Expr.mvar n => n | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.mvarId!" 1072 14 "mvar expected"
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.
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.
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.
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.
Equations
- Lean.Expr.consumeMData (Lean.Expr.mdata data expr) = Lean.Expr.consumeMData expr
- Lean.Expr.consumeMData _fun_discr = _fun_discr
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.
Equations
- One or more equations did not get rendered due to their size.
Equations
Return true
if e
is a non-dependent arrow.
Remark: the following function assumes e
does not have loose bound variables.
Equations
- Lean.Expr.isArrow e = match e with | Lean.Expr.forallE binderName binderType b binderInfo => !Lean.Expr.hasLooseBVars b | x => false
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 _fun_discr _fun_discr _fun_discr = (_fun_discr && Lean.Expr.hasLooseBVar _fun_discr _fun_discr)
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
.
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 fvar
in e
with v
Equations
- Lean.Expr.replaceFVar e fvar v = Lean.Expr.instantiate1 (Lean.Expr.abstract e #[fvar]) v
Replace occurrences of the free variable fvarId
in e
with v
Equations
- Lean.Expr.replaceFVarId e fvarId v = Lean.Expr.replaceFVar e (Lean.mkFVar fvarId) v
Replace occurrences of the free variables fvars
in e
with vs
Equations
- Lean.Expr.replaceFVars e fvars vs = Lean.Expr.instantiateRev (Lean.Expr.abstract e fvars) vs
Equations
- Lean.Expr.instToStringExpr = { toString := Lean.Expr.dbgToString }
Returns true when the expression does not have any sub-expressions.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.mkDecIsTrue pred proof = Lean.mkAppB (Lean.mkConst (Lean.Name.mkStr2 "Decidable" "isTrue")) pred proof
Equations
- Lean.mkDecIsFalse pred proof = Lean.mkAppB (Lean.mkConst (Lean.Name.mkStr2 "Decidable" "isFalse")) pred proof
Equations
Equations
Equations
Equations
- Lean.instInhabitedExprStructEq = { default := { val := default } }
Equations
- Lean.instCoeExprExprStructEq = { coe := Lean.ExprStructEq.mk }
Equations
- Lean.ExprStructEq.beq _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := e₁ }, { val := e₂ } => Lean.Expr.equal e₁ e₂
Equations
- Lean.ExprStructEq.hash _fun_discr = match _fun_discr with | { val := e } => Lean.Expr.hash e
Equations
Equations
Equations
- Lean.ExprStructEq.instToStringExprStructEq = { toString := fun e => toString e.val }
Equations
Equations
mkAppRevRange f b e args == mkAppRev f (revArgs.extract b e)
Equations
- Lean.Expr.mkAppRevRange f beginIdx endIdx revArgs = Lean.Expr.mkAppRevRangeAux revArgs beginIdx f endIdx
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.
Equations
- Lean.Expr.betaRev f revArgs useZeta preserveMData = if (Array.size revArgs == 0) = true then f else let sz := Array.size revArgs; Lean.Expr.betaRev.go revArgs useZeta preserveMData sz f 0
Apply the given arguments to f
, beta-reducing if f
is a
lambda expression. See docstring for betaRev
for examples.
Equations
- Lean.Expr.beta f args = Lean.Expr.betaRev f (Array.reverse args) false
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 _fun_discr = false
(fun x => e) a
==> e[x/a]
.
Equations
- Lean.Expr.headBeta e = let f := Lean.Expr.getAppFn e; if Lean.Expr.isHeadBetaTargetFn false f = true then Lean.Expr.betaRev f (Lean.Expr.getAppRevArgs e) false else e
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.
Equations
- Lean.Expr.isHeadBetaTarget e useZeta = (Lean.Expr.isApp e && Lean.Expr.isHeadBetaTargetFn useZeta (Lean.Expr.getAppFn e))
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
Equations
Similar to etaExpanded?
, but only succeeds if ₙ ≥ 1
.
Equations
- Lean.Expr.etaExpandedStrict? _fun_discr = match _fun_discr with | Lean.Expr.lam binderName binderType b binderInfo => Lean.Expr.etaExpandedAux b 1 | x => none
Return some e'
if e
is of the form optParam _ e'
Equations
- Lean.Expr.getOptParamDefault? e = if Lean.Expr.isAppOfArity e (Lean.Name.mkStr1 "optParam") 2 = true then some (Lean.Expr.appArg! e) else none
Return some e'
if e
is of the form autoParam _ e'
Equations
- Lean.Expr.getAutoParamTactic? e = if Lean.Expr.isAppOfArity e (Lean.Name.mkStr1 "autoParam") 2 = true then some (Lean.Expr.appArg! e) else none
Return true
if e
is of the form outParam _
Equations
- Lean.Expr.isOutParam e = Lean.Expr.isAppOfArity e (Lean.Name.mkStr1 "outParam") 1
Return true
if e
is of the form optParam _ _
Equations
- Lean.Expr.isOptParam e = Lean.Expr.isAppOfArity e (Lean.Name.mkStr1 "optParam") 2
Return true
if e
is of the form autoParam _ _
Equations
- Lean.Expr.isAutoParam e = Lean.Expr.isAppOfArity e (Lean.Name.mkStr1 "autoParam") 2
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
.
Equations
Return true
if e
contains the given free variable.
Equations
- Lean.Expr.containsFVar e fvarId = Lean.Expr.hasAnyFVar e fun a => a == fvarId
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.
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.
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.
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.
Equations
- Lean.Expr.updateFn (Lean.Expr.app f a) _fun_discr = Lean.Expr.updateApp! (Lean.Expr.app f a) (Lean.Expr.updateFn f _fun_discr) a
- Lean.Expr.updateFn _fun_discr _fun_discr = _fun_discr
Eta reduction. If e
is of the form (fun x => f x)
, then return f
.
Instantiate level parameters
Instantiate univeres level parameters names paramNames
with lvls
in e
.
If the two lists have different length, the smallest one is used.
Equations
- Lean.Expr.instantiateLevelParams e paramNames lvls = Lean.Expr.instantiateLevelParamsCore (Lean.Expr.getParamSubst paramNames lvls) e
Instantiate univeres level parameters names paramNames
with lvls
in e
.
If the two arrays have different length, the smallest one is used.
Equations
- Lean.Expr.instantiateLevelParamsArray e paramNames lvls = Lean.Expr.instantiateLevelParamsCore (fun p => Lean.Expr.getParamSubstArray paramNames lvls p 0) e
Annotate e
with the given option.
The information is stored using metadata around e
.
Equations
- Lean.Expr.setOption e optionName val = Lean.mkMData (Lean.KVMap.set Lean.MData.empty optionName val) e
Annotate e
with pp.explicit := flag
The delaborator uses pp
options.
Equations
- Lean.Expr.setPPExplicit e flag = Lean.Expr.setOption e (Lean.Name.mkStr2 "pp" "explicit") flag
Annotate e
with pp.universes := flag
The delaborator uses pp
options.
Equations
- Lean.Expr.setPPUniverses e flag = Lean.Expr.setOption e (Lean.Name.mkStr2 "pp" "universes") flag
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
.
Equations
- One or more equations did not get rendered due to their size.
Similar for setAppPPExplicit
, but only annotate children with pp.explicit := false
if
e
does not contain metavariables.
Equations
- One or more equations did not get rendered due to their size.
Annotate e
with the given annotation name kind
.
It uses metadata to store the annotation.
Equations
- Lean.mkAnnotation kind e = Lean.mkMData (Lean.KVMap.insert Lean.KVMap.empty kind (Lean.DataValue.ofBool true)) e
Return some e'
if e = mkAnnotation kind e'
Equations
- Lean.annotation? kind e = match e with | Lean.Expr.mdata d b => if (Lean.KVMap.size d == 1 && Lean.KVMap.getBool d kind) = true then some b else none | x => none
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
Equations
- Lean.mkLetFunAnnotation e = Lean.mkAnnotation (Lean.Name.mkStr1 "let_fun") e
Return some e'
if e = mkLetFunAnnotation e'
Equations
- Lean.letFunAnnotation? e = Lean.annotation? (Lean.Name.mkStr1 "let_fun") e
Return true if e = mkLetFunAnnotation e'
, and e'
is of the form (fun x : t => b) v
Equations
- Lean.isLetFun e = match Lean.letFunAnnotation? e with | none => false | some e => Lean.Expr.isApp e && Lean.Expr.isLambda (Lean.Expr.appFn! e)
Auxiliary annotation used to mark terms marked with the "inaccessible" annotation .(t)
and
_
in patterns.
Equations
- Lean.mkInaccessible e = Lean.mkAnnotation (Lean.Name.mkStr1 "_inaccessible") e
Return some e'
if e = mkInaccessible e'
.
Equations
- Lean.inaccessible? e = Lean.annotation? (Lean.Name.mkStr1 "_inaccessible") e
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
Equations
- One or more equations did not get rendered due to their size.
Annotate the pattern p
with stx
. This is an auxiliary annotation
for producing better hover information.
Equations
- One or more equations did not get rendered due to their size.
Return some p
if e
is an annotated pattern (inaccessible?
or patternWithRef?
)
Equations
- Lean.patternAnnotation? e = match Lean.inaccessible? e with | some e => some e | x => match Lean.patternWithRef? e with | some (fst, e) => some e | x => none
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.
Equations
- Lean.mkLHSGoalRaw e = Lean.mkAnnotation (Lean.Name.mkStr1 "_lhsGoal") e
Return some lhs
if e = mkLHSGoal e'
, where e'
is of the form lhs = rhs
.
Equations
- One or more equations did not get rendered due to their size.
Polymorphic operation for generating unique/fresh free variable identifiers.
It is available in any monad m
that implements the inferface MonadNameGenerator
.
Polymorphic operation for generating unique/fresh metavariable identifiers.
It is available in any monad m
that implements the inferface MonadNameGenerator
.
Polymorphic operation for generating unique/fresh universe metavariable identifiers.
It is available in any monad m
that implements the inferface MonadNameGenerator
.
Return Not p
Equations
- Lean.mkNot p = Lean.mkApp (Lean.mkConst (Lean.Name.mkStr1 "Not")) p
Return p ∨ q
Equations
- Lean.mkOr p q = Lean.mkApp2 (Lean.mkConst (Lean.Name.mkStr1 "Or")) p q
Return p ∧ q
Equations
- Lean.mkAnd p q = Lean.mkApp2 (Lean.mkConst (Lean.Name.mkStr1 "And")) p q
Return Classical.em p
Equations
- Lean.mkEM p = Lean.mkApp (Lean.mkConst (Lean.Name.mkStr2 "Classical" "em")) p