Documentation

instance Lean.instInhabitedBinderInfo :

Inhabited BinderInfo

Equations

Lean.instInhabitedBinderInfo = { default := Lean.BinderInfo.default }

instance Lean.instBEqBinderInfo :

BEq BinderInfo

Equations

Lean.instBEqBinderInfo = { beq := Lean.beqBinderInfo✝ }

instance Lean.instReprBinderInfo :

Repr BinderInfo

Equations

Lean.instReprBinderInfo = { reprPrec := Lean.reprBinderInfo✝ }

def Lean.BinderInfo.hash :

BinderInfo → UInt64

Equations

Lean.BinderInfo.default.hash = 947
Lean.BinderInfo.implicit.hash = 1019
Lean.BinderInfo.strictImplicit.hash = 1087
Lean.BinderInfo.instImplicit.hash = 1153

def Lean.BinderInfo.isExplicit :

Return true if the given BinderInfo does not correspond to an implicit binder annotation (i.e., implicit, strictImplicit, or instImplicit).

Equations

instance Lean.instHashableBinderInfo :

Hashable BinderInfo

Equations

Lean.instHashableBinderInfo = { hash := Lean.BinderInfo.hash }

def Lean.BinderInfo.isInstImplicit :

Return true if the given BinderInfo is an instance implicit annotation (e.g., [Decidable α])

Equations

def Lean.BinderInfo.isImplicit :

Return true if the given BinderInfo is a regular implicit annotation (e.g., {α : Type u})

Equations

Lean.BinderInfo.implicit.isImplicit = true
x✝.isImplicit = false

def Lean.BinderInfo.isStrictImplicit :

Return true if the given BinderInfo is a strict implicit annotation (e.g., {{α : Type u}})

Equations

@[reducible, inline]

abbrev Lean.MData :

Expression metadata. Used with the Expr.mdata constructor.

Equations

Lean.MData = Lean.KVMap

@[reducible, inline]

abbrev Lean.MData.empty :

MData

Equations

Lean.MData.empty = { entries := [] }

def Lean.Expr.Data :

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

Lean.Expr.Data = UInt64

Instances For

instance Lean.instInhabitedData_1 :

Inhabited Expr.Data

Equations

Lean.instInhabitedData_1 = inferInstanceAs (Inhabited UInt64)

def Lean.Expr.Data.hash (c : Data) :

UInt64

Equations

c.hash = (UInt64.toUInt32 c).toUInt64

instance Lean.instBEqData_1 :

BEq Expr.Data

Equations

Lean.instBEqData_1 = { beq := fun (a b : UInt64) => a == b }

def Lean.Expr.Data.approxDepth (c : Data) :

UInt8

Equations

c.approxDepth = ((UInt64.shiftRight c 32).land 255).toUInt8

def Lean.Expr.Data.looseBVarRange (c : Data) :

UInt32

Equations

c.looseBVarRange = (UInt64.shiftRight c 44).toUInt32

def Lean.Expr.Data.hasFVar (c : Data) :

Equations

c.hasFVar = ((UInt64.shiftRight c 40).land 1 == 1)

def Lean.Expr.Data.hasExprMVar (c : Data) :

Equations

c.hasExprMVar = ((UInt64.shiftRight c 41).land 1 == 1)

def Lean.Expr.Data.hasLevelMVar (c : Data) :

Equations

c.hasLevelMVar = ((UInt64.shiftRight c 42).land 1 == 1)

def Lean.Expr.Data.hasLevelParam (c : Data) :

Equations

c.hasLevelParam = ((UInt64.shiftRight c 43).land 1 == 1)

@[extern lean_uint8_to_uint64]

def Lean.BinderInfo.toUInt64 :

BinderInfo → UInt64

Equations

def Lean.Expr.mkData (h : UInt64) (looseBVarRange : Nat := 0) (approxDepth : UInt32 := 0) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool := false) :

Equations

One or more equations did not get rendered due to their size.

@[inline]

def Lean.Expr.mkAppData (fData aData : Data) :

Optimized version of Expr.mkData for applications.

Equations

One or more equations did not get rendered due to their size.

@[inline]

def Lean.Expr.mkDataForBinder (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt32) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool) :

Equations

Lean.Expr.mkDataForBinder h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam = Lean.Expr.mkData h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam

@[inline]

def Lean.Expr.mkDataForLet (h : UInt64) (looseBVarRange : Nat) (approxDepth : UInt32) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool) :

Equations

Lean.Expr.mkDataForLet h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam = Lean.Expr.mkData h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam

instance Lean.instReprData_1 :

Repr Expr.Data

Equations

One or more equations did not get rendered due to their size.

structure Lean.FVarId :

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.

name : Name

Instances For

instance Lean.instInhabitedFVarId :

Inhabited FVarId

Equations

Lean.instInhabitedFVarId = { default := { name := default } }

instance Lean.instBEqFVarId :

BEq FVarId

Equations

Lean.instBEqFVarId = { beq := Lean.beqFVarId✝ }

instance Lean.instHashableFVarId :

Hashable FVarId

Equations

Lean.instHashableFVarId = { hash := Lean.hashFVarId✝ }

instance Lean.instReprFVarId :

Repr FVarId

Equations

Lean.instReprFVarId = { reprPrec := fun (n : Lean.FVarId) (p : Nat) => reprPrec n.name p }

def Lean.FVarIdSet :

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 (x1 x2 : Lean.FVarId) => x1.name.quickCmp x2.name

Instances For

instance Lean.instFVarIdSetInhabited :

Inhabited FVarIdSet

Equations

Lean.instFVarIdSetInhabited = Lean.instInhabitedRBTree

EmptyCollection FVarIdSet

instance Lean.instFVarIdSetEmptyCollection :

Equations

Lean.instFVarIdSetEmptyCollection = Lean.instEmptyCollectionRBTree Lean.FVarId fun (x1 x2 : Lean.FVarId) => x1.name.quickCmp x2.name

instance Lean.instForInFVarIdSetFVarId {m : Type u_1 → Type u_2} :

ForIn m FVarIdSet FVarId

Equations

Lean.instForInFVarIdSetFVarId = inferInstanceAs (ForIn m (Lean.RBTree Lean.FVarId fun (x1 x2 : Lean.FVarId) => x1.name.quickCmp x2.name) Lean.FVarId)

def Lean.FVarIdSet.insert (s : FVarIdSet) (fvarId : FVarId) :

FVarIdSet

Equations

s.insert fvarId = Lean.RBTree.insert s fvarId

def Lean.FVarIdHashSet :

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

Lean.FVarIdHashSet = Std.HashSet Lean.FVarId

Instances For

instance Lean.instFVarIdHashSetInhabited :

Inhabited FVarIdHashSet

Equations

Lean.instFVarIdHashSetInhabited = Std.HashSet.instInhabited

EmptyCollection FVarIdHashSet

instance Lean.instFVarIdHashSetEmptyCollection :

Equations

Lean.instFVarIdHashSetEmptyCollection = Std.HashSet.instEmptyCollection

def Lean.FVarIdMap (α : Type) :

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 (x1 x2 : Lean.FVarId) => x1.name.quickCmp x2.name

Instances For

def Lean.FVarIdMap.insert {α : Type} (s : FVarIdMap α) (fvarId : FVarId) (a : α) :

FVarIdMap α

Equations

s.insert fvarId a = Lean.RBMap.insert s fvarId a

instance Lean.instEmptyCollectionFVarIdMap {α : Type} :

EmptyCollection (FVarIdMap α)

Equations

Lean.instEmptyCollectionFVarIdMap = inferInstanceAs (EmptyCollection (Lean.RBMap Lean.FVarId α fun (x1 x2 : Lean.FVarId) => x1.name.quickCmp x2.name))

instance Lean.instInhabitedFVarIdMap {α : Type} :

Inhabited (FVarIdMap α)

Equations

Lean.instInhabitedFVarIdMap = { default := ∅ }

structure Lean.MVarId :

Universe metavariable Id

name : Name

Instances For

instance Lean.instInhabitedMVarId :

Inhabited MVarId

Equations

Lean.instInhabitedMVarId = { default := { name := default } }

instance Lean.instBEqMVarId :

BEq MVarId

Equations

Lean.instBEqMVarId = { beq := Lean.beqMVarId✝ }

instance Lean.instHashableMVarId :

Hashable MVarId

Equations

Lean.instHashableMVarId = { hash := Lean.hashMVarId✝ }

instance Lean.instReprMVarId :

Repr MVarId

Equations

Lean.instReprMVarId = { reprPrec := Lean.reprMVarId✝ }

instance Lean.instReprMVarId_1 :

Repr MVarId

Equations

Lean.instReprMVarId_1 = { reprPrec := fun (n : Lean.MVarId) (p : Nat) => reprPrec n.name p }

def Lean.MVarIdSet :

Equations

Lean.MVarIdSet = Lean.RBTree Lean.MVarId fun (x1 x2 : Lean.MVarId) => x1.name.quickCmp x2.name

Instances For

instance Lean.instMVarIdSetInhabited :

Inhabited MVarIdSet

Equations

Lean.instMVarIdSetInhabited = Lean.instInhabitedRBTree

EmptyCollection MVarIdSet

instance Lean.instMVarIdSetEmptyCollection :

Equations

Lean.instMVarIdSetEmptyCollection = Lean.instEmptyCollectionRBTree Lean.MVarId fun (x1 x2 : Lean.MVarId) => x1.name.quickCmp x2.name

def Lean.MVarIdSet.insert (s : MVarIdSet) (mvarId : MVarId) :

MVarIdSet

Equations

s.insert mvarId = Lean.RBTree.insert s mvarId

instance Lean.instForInMVarIdSetMVarId {m : Type u_1 → Type u_2} :

ForIn m MVarIdSet MVarId

Equations

Lean.instForInMVarIdSetMVarId = inferInstanceAs (ForIn m (Lean.RBTree Lean.MVarId fun (x1 x2 : Lean.MVarId) => x1.name.quickCmp x2.name) Lean.MVarId)

def Lean.MVarIdMap (α : Type) :

Equations

Lean.MVarIdMap α = Lean.RBMap Lean.MVarId α fun (x1 x2 : Lean.MVarId) => x1.name.quickCmp x2.name

Instances For

def Lean.MVarIdMap.insert {α : Type} (s : MVarIdMap α) (mvarId : MVarId) (a : α) :

MVarIdMap α

Equations

s.insert mvarId a = Lean.RBMap.insert s mvarId a

instance Lean.instEmptyCollectionMVarIdMap {α : Type} :

EmptyCollection (MVarIdMap α)

Equations

Lean.instEmptyCollectionMVarIdMap = inferInstanceAs (EmptyCollection (Lean.RBMap Lean.MVarId α fun (x1 x2 : Lean.MVarId) => x1.name.quickCmp x2.name))

instance Lean.instForInMVarIdMapProdMVarId {m : Type u_1 → Type u_2} {α : Type} :

ForIn m (MVarIdMap α) (MVarId × α)

Equations

Lean.instForInMVarIdMapProdMVarId = inferInstanceAs (ForIn m (Lean.RBMap Lean.MVarId α fun (x1 x2 : Lean.MVarId) => x1.name.quickCmp x2.name) (Lean.MVarId × α))

instance Lean.instInhabitedMVarIdMap {α : Type} :

Inhabited (MVarIdMap α)

Equations

Lean.instInhabitedMVarIdMap = { default := ∅ }

inductive Lean.Expr :

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.

bvar (deBruijnIndex : Nat) : 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 a lam, forallE, or letE).
The deBruijnIndex parameter is the de-Bruijn index for the bound variable. See the Wikipedia page on de-Bruijn indices for additional information.
For example, consider the expression fun x : Nat => forall y : Nat, x = y. The x and y variables in the equality expression are constructed using bvar and bound to the binders introduced by the earlier lam and forallE constructors. Here is the corresponding Expr 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 (fvarId : FVarId) : Expr
The fvar constructor represent free variables. These free variable occurrences are not bound by an earlier lam, forallE, or letE constructor and its binder exists in a local context only.
Note that Lean uses the locally nameless approach. See McBride and McKinna for additional details.
When "visiting" the body of a binding expression (i.e. lam, forallE, or letE), bound variables are converted into free variables using a unique identifier, and their user-facing name, type, value (for LetE), and binder annotation are stored in the LocalContext.
mvar (mvarId : MVarId) : 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 (u : Level) : Expr
Used for Type u, Sort u, and Prop:
- Prop is represented as .sort .zero,
- Sort u as .sort (.param `u), and
- Type u as .sort (.succ (.param `u))
const (declName : Name) (us : List Level) : Expr
A (universe polymorphic) constant that has been defined earlier in the module or by another imported module. For example, @Eq.{1} is represented as Expr.const `Eq [.succ .zero], and @Array.map.{0, 0} is represented as Expr.const `Array.map [.zero, .zero].
app (fn arg : Expr) : Expr
A function application.
For example, the natural number one, i.e. Nat.succ Nat.zero is represented as Expr.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 as Expr.app (.app f x) y.
lam (binderName : Name) (binderType body : Expr) (binderInfo : BinderInfo) : 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 as
```
Expr.lam `x (.const `Nat []) (.bvar 0) .default
```
forallE (binderName : Name) (binderType body : Expr) (binderInfo : BinderInfo) : Expr
A dependent arrow (a : α) → β) (aka forall-expression) where β may dependent on a. Note that this constructor is also used to represent non-dependent arrows where β does not depend on a.
For example:
- forall x : Prop, x ∧ x:
```
Expr.forallE `x (.sort .zero)
  (.app (.app (.const `And []) (.bvar 0)) (.bvar 0)) .default
```
- Nat → Bool:
```
Expr.forallE `a (.const `Nat [])
  (.const `Bool []) .default
```
letE (declName : Name) (type value body : Expr) (nonDep : Bool) : 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. In contrast, the dependent let-expression let 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 as
```
Expr.letE `x (.const `Nat []) (.lit (.natVal 2)) (.app (.const `Nat.succ []) (.bvar 0)) true
```
lit : Literal → 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 as Expr.lit (.natVal 2). Note that, it is definitionally equal to:
```
Expr.app (.const `Nat.succ []) (.app (.const `Nat.succ []) (.const `Nat.zero []))
```
mdata (data : MData) (expr : Expr) : 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 the inaccessible annotation during elaboration to mark Exprs that correspond to inaccessible patterns).
Note that Expr.mdata data e is definitionally equal to e.
proj (typeName : Name) (idx : Nat) (struct : Expr) : 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 the typeName matches the type of struct, and whether the (zero-based) index is valid (i.e., it is smaller than the number of constructor fields). When exporting Lean developments to other systems, proj can be replaced with typeName.rec applications.
Example, given a : Nat × Bool, a.1 is represented as
```
.proj `Prod 0 a
```

Instances For

@[extern lean_expr_data]

noncomputable def Lean.Expr.data :

Expr → Data

Equations

One or more equations did not get rendered due to their size.
(Lean.Expr.const n lvls).data = Lean.Expr.mkData (mixHash 5 (mixHash (hash n) (hash lvls))) 0 0 false false (lvls.any Lean.Level.hasMVar) (lvls.any Lean.Level.hasParam)
(Lean.Expr.bvar idx).data = Lean.Expr.mkData (mixHash 7 (hash idx)) (idx + 1)
(Lean.Expr.sort lvl).data = Lean.Expr.mkData (mixHash 11 (hash lvl)) 0 0 false false lvl.hasMVar lvl.hasParam
(Lean.Expr.fvar fvarId).data = Lean.Expr.mkData (mixHash 13 (hash fvarId)) 0 0 true
(Lean.Expr.mvar fvarId).data = Lean.Expr.mkData (mixHash 17 (hash fvarId)) 0 0 false true
(f.app a).data = Lean.Expr.mkAppData f.data a.data
(Lean.Expr.lit l).data = Lean.Expr.mkData (mixHash 3 (hash l))

instance Lean.instReprExpr :

Repr Expr

Equations

Lean.instReprExpr = { reprPrec := Lean.reprExpr✝ }

instance Lean.instInhabitedExpr :

Inhabited Expr

Equations

Lean.instInhabitedExpr = { default := Lean.Expr.const `_inhabitedExprDummy [] }

def Lean.Expr.ctorName :

Expr → String

The constructor name for the given expression. This is used for debugging purposes.

Equations

(Lean.Expr.bvar a).ctorName = "bvar"
(Lean.Expr.fvar a).ctorName = "fvar"
(Lean.Expr.mvar a).ctorName = "mvar"
(Lean.Expr.sort a).ctorName = "sort"
(Lean.Expr.const a a_1).ctorName = "const"
(a.app a_1).ctorName = "app"
(Lean.Expr.lam a a_1 a_2 a_3).ctorName = "lam"
(Lean.Expr.forallE a a_1 a_2 a_3).ctorName = "forallE"
(Lean.Expr.letE a a_1 a_2 a_3 a_4).ctorName = "letE"
(Lean.Expr.lit a).ctorName = "lit"
(Lean.Expr.mdata a a_1).ctorName = "mdata"
(Lean.Expr.proj a a_1 a_2).ctorName = "proj"

def Lean.Expr.hash (e : Expr) :

UInt64

Equations

e.hash = e.data.hash

instance Lean.Expr.instHashable :

Hashable Expr

Equations

Lean.Expr.instHashable = { hash := Lean.Expr.hash }

def Lean.Expr.hasFVar (e : Expr) :

Return true if e contains free variables. This is a constant time operation.

Equations

e.hasFVar = e.data.hasFVar

def Lean.Expr.hasExprMVar (e : Expr) :

Return true if e contains expression metavariables. This is a constant time operation.

Equations

e.hasExprMVar = e.data.hasExprMVar

def Lean.Expr.hasLevelMVar (e : Expr) :

Return true if e contains universe (aka Level) metavariables. This is a constant time operation.

Equations

e.hasLevelMVar = e.data.hasLevelMVar

def Lean.Expr.hasMVar (e : Expr) :

Does the expression contain level (aka universe) or expression metavariables? This is a constant time operation.

Equations

e.hasMVar = (e.data.hasExprMVar || e.data.hasLevelMVar)

def Lean.Expr.hasLevelParam (e : Expr) :

Return true if e contains universe level parameters. This is a constant time operation.

Equations

e.hasLevelParam = e.data.hasLevelParam

def Lean.Expr.approxDepth (e : Expr) :

UInt32

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

e.approxDepth = e.data.approxDepth.toUInt32

def Lean.Expr.looseBVarRange (e : Expr) :

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

e.looseBVarRange = e.data.looseBVarRange.toNat

def Lean.Expr.binderInfo (e : Expr) :

BinderInfo

Return the binder information if e is a lambda or forall expression, and .default otherwise.

Equations

(Lean.Expr.forallE binderName binderType body bi).binderInfo = bi
(Lean.Expr.lam binderName binderType body bi).binderInfo = bi
e.binderInfo = Lean.BinderInfo.default

Export functions.

@[export lean_expr_hash]

def Lean.Expr.hashEx :

Expr → UInt64

Equations

Lean.Expr.hashEx = hash

@[export lean_expr_has_fvar]

def Lean.Expr.hasFVarEx :

Expr → Bool

Equations

Lean.Expr.hasFVarEx = Lean.Expr.hasFVar

@[export lean_expr_has_expr_mvar]

def Lean.Expr.hasExprMVarEx :

Expr → Bool

Equations

Lean.Expr.hasExprMVarEx = Lean.Expr.hasExprMVar

@[export lean_expr_has_level_mvar]

def Lean.Expr.hasLevelMVarEx :

Expr → Bool

Equations

Lean.Expr.hasLevelMVarEx = Lean.Expr.hasLevelMVar

@[export lean_expr_has_mvar]

def Lean.Expr.hasMVarEx :

Expr → Bool

Equations

Lean.Expr.hasMVarEx = Lean.Expr.hasMVar

@[export lean_expr_has_level_param]

def Lean.Expr.hasLevelParamEx :

Expr → Bool

Equations

Lean.Expr.hasLevelParamEx = Lean.Expr.hasLevelParam

@[export lean_expr_loose_bvar_range]

def Lean.Expr.looseBVarRangeEx (e : Expr) :

UInt32

Equations

e.looseBVarRangeEx = e.data.looseBVarRange

@[export lean_expr_binder_info]

def Lean.Expr.binderInfoEx :

Expr → BinderInfo

Equations

Lean.Expr.binderInfoEx = Lean.Expr.binderInfo

def Lean.mkConst (declName : Name) (us : List Level := []) :

mkConst declName us return .const declName us.

Equations

Lean.mkConst declName us = Lean.Expr.const declName us

def Lean.Literal.type :

Literal → Expr

Return the type of a literal value.

Equations

(Lean.Literal.natVal a).type = Lean.mkConst `Nat
(Lean.Literal.strVal a).type = Lean.mkConst `String

@[export lean_lit_type]

def Lean.Literal.typeEx :

Literal → Expr

Equations

Lean.Literal.typeEx = Lean.Literal.type

def Lean.mkBVar (idx : Nat) :

.bvar idx is now the preferred form.

Equations

Lean.mkBVar idx = Lean.Expr.bvar idx

def Lean.mkSort (u : Level) :

.sort u is now the preferred form.

Equations

Lean.mkSort u = Lean.Expr.sort u

def Lean.mkFVar (fvarId : FVarId) :

.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

def Lean.mkMVar (mvarId : MVarId) :

.mvar mvarId is now the preferred form. This function is seldom used, metavariables are often created using functions such as mkFreshExprMVar at MetaM.

Equations

Lean.mkMVar mvarId = Lean.Expr.mvar mvarId

def Lean.mkMData (m : MData) (e : Expr) :

.mdata m e is now the preferred form.

Equations

Lean.mkMData m e = Lean.Expr.mdata m e

def Lean.mkProj (structName : Name) (idx : Nat) (struct : Expr) :

.proj structName idx struct is now the preferred form.

Equations

Lean.mkProj structName idx struct = Lean.Expr.proj structName idx struct

@[match_pattern]

def Lean.mkApp (f a : Expr) :

.app f a is now the preferred form.

Equations

Lean.mkApp f a = f.app a

def Lean.mkLambda (x : Name) (bi : BinderInfo) (t b : Expr) :

.lam x t b bi is now the preferred form.

Equations

Lean.mkLambda x bi t b = Lean.Expr.lam x t b bi

def Lean.mkForall (x : Name) (bi : BinderInfo) (t b : Expr) :

.forallE x t b bi is now the preferred form.

Equations

Lean.mkForall x bi t b = Lean.Expr.forallE x t b bi

def Lean.mkSimpleThunkType (type : Expr) :

Return Unit -> type. Do not confuse with Thunk type

Equations

Lean.mkSimpleThunkType type = Lean.mkForall Lean.Name.anonymous Lean.BinderInfo.default (Lean.mkConst `Unit) type

def Lean.mkSimpleThunk (type : Expr) :

Return fun (_ : Unit), e

Equations

Lean.mkSimpleThunk type = Lean.mkLambda `_ Lean.BinderInfo.default (Lean.mkConst `Unit) type

def Lean.mkLet (x : Name) (t v b : Expr) (nonDep : Bool := false) :

.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

@[match_pattern]

def Lean.mkAppB (f a b : Expr) :

Equations

Lean.mkAppB f a b = Lean.mkApp (Lean.mkApp f a) b

@[match_pattern]

def Lean.mkApp2 (f a b : Expr) :

Equations

Lean.mkApp2 f a b = Lean.mkAppB f a b

@[match_pattern]

def Lean.mkApp3 (f a b c : Expr) :

Equations

Lean.mkApp3 f a b c = Lean.mkApp (Lean.mkAppB f a b) c

@[match_pattern]

def Lean.mkApp4 (f a b c d : Expr) :

Equations

Lean.mkApp4 f a b c d = Lean.mkAppB (Lean.mkAppB f a b) c d

@[match_pattern]

def Lean.mkApp5 (f a b c d e : Expr) :

Equations

Lean.mkApp5 f a b c d e = Lean.mkApp (Lean.mkApp4 f a b c d) e

@[match_pattern]

def Lean.mkApp6 (f a b c d e₁ e₂ : Expr) :

Equations

Lean.mkApp6 f a b c d e₁ e₂ = Lean.mkAppB (Lean.mkApp4 f a b c d) e₁ e₂

@[match_pattern]

def Lean.mkApp7 (f a b c d e₁ e₂ e₃ : Expr) :

Equations

Lean.mkApp7 f a b c d e₁ e₂ e₃ = Lean.mkApp3 (Lean.mkApp4 f a b c d) e₁ e₂ e₃

@[match_pattern]

def Lean.mkApp8 (f a b c d e₁ e₂ e₃ e₄ : Expr) :

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₄

@[match_pattern]

def Lean.mkApp9 (f a b c d e₁ e₂ e₃ e₄ e₅ : Expr) :

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₅

@[match_pattern]

def Lean.mkApp10 (f a b c d e₁ e₂ e₃ e₄ e₅ e₆ : Expr) :

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₆

def Lean.mkLit (l : Literal) :

.lit l is now the preferred form.

Equations

Lean.mkLit l = Lean.Expr.lit l

def Lean.mkRawNatLit (n : Nat) :

Return the "raw" natural number .lit (.natVal n). This is not the default representation used by the Lean frontend. See mkNatLit.

Equations

Lean.mkRawNatLit n = Lean.mkLit (Lean.Literal.natVal n)

def Lean.mkNatLit (n : Nat) :

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

Lean.mkNatLit n = Lean.mkApp3 (Lean.mkConst `OfNat.ofNat [Lean.levelZero ]) (Lean.mkConst `Nat) (Lean.mkRawNatLit n) (Lean.mkApp (Lean.mkConst `instOfNatNat) (Lean.mkRawNatLit n))

def Lean.mkStrLit (s : String) :

Return the string literal .lit (.strVal s)

Equations

Lean.mkStrLit s = Lean.mkLit (Lean.Literal.strVal s)

@[export lean_expr_mk_bvar]

def Lean.mkBVarEx :

Nat → Expr

Equations

Lean.mkBVarEx = Lean.mkBVar

@[export lean_expr_mk_fvar]

def Lean.mkFVarEx :

FVarId → Expr

Equations

Lean.mkFVarEx = Lean.mkFVar

@[export lean_expr_mk_mvar]

def Lean.mkMVarEx :

MVarId → Expr

Equations

Lean.mkMVarEx = Lean.mkMVar

@[export lean_expr_mk_sort]

def Lean.mkSortEx :

Level → Expr

Equations

Lean.mkSortEx = Lean.mkSort

@[export lean_expr_mk_const]

def Lean.mkConstEx (c : Name) (lvls : List Level) :

Equations

Lean.mkConstEx c lvls = Lean.mkConst c lvls

@[export lean_expr_mk_app]

def Lean.mkAppEx :

Expr → Expr → Expr

Equations

Lean.mkAppEx = Lean.mkApp

@[export lean_expr_mk_lambda]

def Lean.mkLambdaEx (n : Name) (d b : Expr) (bi : BinderInfo) :

Equations

Lean.mkLambdaEx n d b bi = Lean.mkLambda n bi d b

@[export lean_expr_mk_forall]

def Lean.mkForallEx (n : Name) (d b : Expr) (bi : BinderInfo) :

Equations

Lean.mkForallEx n d b bi = Lean.mkForall n bi d b

@[export lean_expr_mk_let]

def Lean.mkLetEx (n : Name) (t v b : Expr) :

Equations

Lean.mkLetEx n t v b = Lean.mkLet n t v b

@[export lean_expr_mk_lit]

def Lean.mkLitEx :

Literal → Expr

Equations

Lean.mkLitEx = Lean.mkLit

@[export lean_expr_mk_mdata]

def Lean.mkMDataEx :

MData → Expr → Expr

Equations

Lean.mkMDataEx = Lean.mkMData

@[export lean_expr_mk_proj]

def Lean.mkProjEx :

Name → Nat → Expr → Expr

Equations

Lean.mkProjEx = Lean.mkProj

def Lean.mkAppN (f : Expr) (args : Array Expr) :

mkAppN f #[a₀, ..., aₙ] constructs the application f a₀ a₁ ... aₙ.

Equations

Lean.mkAppN f args = Array.foldl Lean.mkApp f args

def Lean.mkAppRange (f : Expr) (i j : Nat) (args : Array Expr) :

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

def Lean.mkAppRev (fn : Expr) (revArgs : Array Expr) :

Same as mkApp f args but reversing args.

Equations

Lean.mkAppRev fn revArgs = Array.foldr (fun (a r : Lean.Expr) => Lean.mkApp r a) fn revArgs

@[extern lean_expr_dbg_to_string]

opaque Lean.Expr.dbgToString (e : Expr) :

String

@[extern lean_expr_quick_lt]

opaque Lean.Expr.quickLt (a b : Expr) :

A total order for expressions. We say it is quick because it first compares the hashcodes.

@[extern lean_expr_lt]

opaque Lean.Expr.lt (a b : Expr) :

A total order for expressions that takes the structure into account (e.g., variable names).

def Lean.Expr.quickComp (a b : Expr) :

Ordering

Equations

a.quickComp b = if a.quickLt b = true then Ordering.lt else if b.quickLt a = true then Ordering.gt else Ordering.eq

@[extern lean_expr_eqv]

opaque Lean.Expr.eqv (a b : Expr) :

Return true iff a and b are alpha equivalent. Binder annotations are ignored.

instance Lean.Expr.instBEq :

BEq Expr

Equations

Lean.Expr.instBEq = { beq := Lean.Expr.eqv }

@[extern lean_expr_equal]

opaque Lean.Expr.equal (a b : Expr) :

Return true iff a and b are equal. Binder names and annotations are taken into account.

def Lean.Expr.isSort :

Expr → Bool

Return true if the given expression is a .sort ..

Equations

(Lean.Expr.sort u).isSort = true
x✝.isSort = false

def Lean.Expr.isType :

Expr → Bool

Return true if the given expression is of the form .sort (.succ ..).

Equations

(Lean.Expr.sort a.succ).isType = true
x✝.isType = false

def Lean.Expr.isType0 :

Expr → Bool

Return true if the given expression is of the form .sort (.succ .zero).

Equations

(Lean.Expr.sort Lean.Level.zero.succ).isType0 = true
x✝.isType0 = false

def Lean.Expr.isProp :

Expr → Bool

Return true if the given expression is .sort .zero

Equations

(Lean.Expr.sort Lean.Level.zero).isProp = true
x✝.isProp = false

def Lean.Expr.isBVar :

Expr → Bool

Return true if the given expression is a bound variable.

Equations

(Lean.Expr.bvar deBruijnIndex).isBVar = true
x✝.isBVar = false

def Lean.Expr.isMVar :

Expr → Bool

Return true if the given expression is a metavariable.

Equations

(Lean.Expr.mvar mvarId).isMVar = true
x✝.isMVar = false

def Lean.Expr.isFVar :

Expr → Bool

Return true if the given expression is a free variable.

Equations

(Lean.Expr.fvar fvarId).isFVar = true
x✝.isFVar = false

def Lean.Expr.isApp :

Expr → Bool

Return true if the given expression is an application.

Equations

(fn.app arg).isApp = true
x✝.isApp = false

def Lean.Expr.isProj :

Expr → Bool

Return true if the given expression is a projection .proj ..

Equations

(Lean.Expr.proj typeName idx struct).isProj = true
x✝.isProj = false

def Lean.Expr.isConst :

Expr → Bool

Return true if the given expression is a constant.

Equations

(Lean.Expr.const declName us).isConst = true
x✝.isConst = false

def Lean.Expr.isConstOf :

Expr → Name → Bool

Return true if the given expression is a constant of the given name. Examples:

(.const `Nat []).isConstOf `Nat is true
(.const `Nat []).isConstOf `False is false

Equations

(Lean.Expr.const n us).isConstOf x✝ = (n == x✝)
x✝¹.isConstOf x✝ = false

def Lean.Expr.isFVarOf :

Expr → FVarId → Bool

Return true if the given expression is a free variable with the given id. Examples:

isFVarOf (.fvar id) id is true
isFVarOf (.fvar id) id' is false
isFVarOf (.sort levelZero) id is false

Equations

(Lean.Expr.fvar fvarId).isFVarOf x✝ = (fvarId == x✝)
x✝¹.isFVarOf x✝ = false

def Lean.Expr.isForall :

Expr → Bool

Return true if the given expression is a forall-expression aka (dependent) arrow.

Equations

(Lean.Expr.forallE binderName binderType body binderInfo).isForall = true
x✝.isForall = false

def Lean.Expr.isLambda :

Expr → Bool

Return true if the given expression is a lambda abstraction aka anonymous function.

Equations

(Lean.Expr.lam binderName binderType body binderInfo).isLambda = true
x✝.isLambda = false

def Lean.Expr.isBinding :

Expr → Bool

Return true if the given expression is a forall or lambda expression.

Equations

(Lean.Expr.lam binderName binderType body binderInfo).isBinding = true
(Lean.Expr.forallE binderName binderType body binderInfo).isBinding = true
x✝.isBinding = false

def Lean.Expr.isLet :

Expr → Bool

Return true if the given expression is a let-expression.

Equations

(Lean.Expr.letE declName type value body nonDep).isLet = true
x✝.isLet = false

def Lean.Expr.isMData :

Expr → Bool

Return true if the given expression is a metadata.

Equations

(Lean.Expr.mdata data expr).isMData = true
x✝.isMData = false

def Lean.Expr.isLit :

Expr → Bool

Return true if the given expression is a literal value.

Equations

(Lean.Expr.lit a).isLit = true
x✝.isLit = false

def Lean.Expr.appFn! :

Expr → Expr

Equations

(fn.app arg).appFn! = fn
x✝.appFn! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appFn!" 903 15 "application expected"

def Lean.Expr.appArg! :

Expr → Expr

Equations

(fn.app arg).appArg! = arg
x✝.appArg! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appArg!" 907 15 "application expected"

def Lean.Expr.appFn!' :

Expr → Expr

Equations

(Lean.Expr.mdata data b).appFn!' = b.appFn!'
(f.app arg).appFn!' = f
x✝.appFn!' = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appFn!'" 912 17 "application expected"

def Lean.Expr.appArg!' :

Expr → Expr

Equations

(Lean.Expr.mdata data b).appArg!' = b.appArg!'
(f.app arg).appArg!' = arg
x✝.appArg!' = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appArg!'" 917 17 "application expected"

def Lean.Expr.appArg (e : Expr) (h : e.isApp = true) :

Equations

(fn.app a).appArg x = a

def Lean.Expr.appFn (e : Expr) (h : e.isApp = true) :

Equations

(fn.app a).appFn x = fn

def Lean.Expr.sortLevel! :

Expr → Level

Equations

(Lean.Expr.sort u).sortLevel! = u
x✝.sortLevel! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.sortLevel!" 929 14 "sort expected"

def Lean.Expr.litValue! :

Expr → Literal

Equations

(Lean.Expr.lit a).litValue! = a
x✝.litValue! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.litValue!" 933 13 "literal expected"

def Lean.Expr.isRawNatLit :

Expr → Bool

Equations

(Lean.Expr.lit (Lean.Literal.natVal val)).isRawNatLit = true
x✝.isRawNatLit = false

def Lean.Expr.rawNatLit? :

Expr → Option Nat

Equations

(Lean.Expr.lit (Lean.Literal.natVal val)).rawNatLit? = some val
x✝.rawNatLit? = none

def Lean.Expr.isStringLit :

Expr → Bool

Equations

(Lean.Expr.lit (Lean.Literal.strVal val)).isStringLit = true
x✝.isStringLit = false

def Lean.Expr.isCharLit :

Expr → Bool

Equations

((Lean.Expr.const c us).app a).isCharLit = (c == `Char.ofNat && a.isRawNatLit)
x✝.isCharLit = false

def Lean.Expr.constName! :

Expr → Name

Equations

(Lean.Expr.const declName us).constName! = declName
x✝.constName! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.constName!" 953 17 "constant expected"

def Lean.Expr.constName? :

Expr → Option Name

Equations

(Lean.Expr.const declName us).constName? = some declName
x✝.constName? = none

def Lean.Expr.constName (e : Expr) :

Name

If the expression is a constant, return that name. Otherwise return Name.anonymous.

Equations

e.constName = e.constName?.getD Lean.Name.anonymous

def Lean.Expr.constLevels! :

Expr → List Level

Equations

(Lean.Expr.const declName us).constLevels! = us
x✝.constLevels! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.constLevels!" 965 18 "constant expected"

def Lean.Expr.bvarIdx! :

Expr → Nat

Equations

(Lean.Expr.bvar deBruijnIndex).bvarIdx! = deBruijnIndex
x✝.bvarIdx! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.bvarIdx!" 969 16 "bvar expected"

def Lean.Expr.fvarId! :

Expr → FVarId

Equations

(Lean.Expr.fvar fvarId).fvarId! = fvarId
x✝.fvarId! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.fvarId!" 973 14 "fvar expected"

def Lean.Expr.fvarId? :

Expr → Option FVarId

Equations

(Lean.Expr.fvar fvarId).fvarId? = some fvarId
x✝.fvarId? = none

def Lean.Expr.mvarId! :

Expr → MVarId

Equations

(Lean.Expr.mvar mvarId).mvarId! = mvarId
x✝.mvarId! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.mvarId!" 981 14 "mvar expected"

def Lean.Expr.bindingName! :

Expr → Name

Equations

(Lean.Expr.forallE binderName binderType body bi).bindingName! = binderName
(Lean.Expr.lam binderName binderType body bi).bindingName! = binderName
x✝.bindingName! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.bindingName!" 986 23 "binding expected"

def Lean.Expr.bindingDomain! :

Expr → Expr

Equations

(Lean.Expr.forallE binderName binderType body bi).bindingDomain! = binderType
(Lean.Expr.lam binderName binderType body bi).bindingDomain! = binderType
x✝.bindingDomain! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.bindingDomain!" 991 23 "binding expected"

def Lean.Expr.bindingBody! :

Expr → Expr

Equations

(Lean.Expr.forallE binderName binderType body bi).bindingBody! = body
(Lean.Expr.lam binderName binderType body bi).bindingBody! = body
x✝.bindingBody! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.bindingBody!" 996 23 "binding expected"

def Lean.Expr.bindingInfo! :

Expr → BinderInfo

Equations

(Lean.Expr.forallE binderName binderType body bi).bindingInfo! = bi
(Lean.Expr.lam binderName binderType body bi).bindingInfo! = bi
x✝.bindingInfo! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.bindingInfo!" 1001 24 "binding expected"

def Lean.Expr.letName! :

Expr → Name

Equations

(Lean.Expr.letE declName type value body nonDep).letName! = declName
x✝.letName! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.letName!" 1005 17 "let expression expected"

def Lean.Expr.letType! :

Expr → Expr

Equations

(Lean.Expr.letE declName type value body nonDep).letType! = type
x✝.letType! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.letType!" 1009 19 "let expression expected"

def Lean.Expr.letValue! :

Expr → Expr

Equations

(Lean.Expr.letE declName type value body nonDep).letValue! = value
x✝.letValue! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.letValue!" 1013 21 "let expression expected"

def Lean.Expr.letBody! :

Expr → Expr

Equations

(Lean.Expr.letE declName type value body nonDep).letBody! = body
x✝.letBody! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.letBody!" 1017 23 "let expression expected"

def Lean.Expr.consumeMData :

Expr → Expr

Equations

(Lean.Expr.mdata data expr).consumeMData = expr.consumeMData
x✝.consumeMData = x✝

def Lean.Expr.mdataExpr! :

Expr → Expr

Equations

(Lean.Expr.mdata data expr).mdataExpr! = expr
x✝.mdataExpr! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.mdataExpr!" 1025 17 "mdata expression expected"

def Lean.Expr.projExpr! :

Expr → Expr

Equations

(Lean.Expr.proj typeName idx struct).projExpr! = struct
x✝.projExpr! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.projExpr!" 1029 18 "proj expression expected"

def Lean.Expr.projIdx! :

Expr → Nat

Equations

(Lean.Expr.proj typeName idx struct).projIdx! = idx
x✝.projIdx! = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.projIdx!" 1033 18 "proj expression expected"

def Lean.Expr.getForallBody :

Expr → Expr

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.forallE binderName binderType body binderInfo).getForallBody = body.getForallBody
x✝.getForallBody = x✝

def Lean.Expr.getForallBodyMaxDepth (maxDepth : Nat) :

Expr → Expr

Equations

Lean.Expr.getForallBodyMaxDepth n.succ (Lean.Expr.forallE binderName binderType b binderInfo) = Lean.Expr.getForallBodyMaxDepth n b
Lean.Expr.getForallBodyMaxDepth 0 x✝ = x✝
Lean.Expr.getForallBodyMaxDepth x✝¹ x✝ = x✝

def Lean.Expr.getForallBinderNames :

Expr → List Name

Given a sequence of nested foralls (a₁ : α₁) → ... → (aₙ : αₙ) → _, returns the names [a₁, ... aₙ].

Equations

(Lean.Expr.forallE binderName binderType body binderInfo).getForallBinderNames = binderName :: body.getForallBinderNames
x✝.getForallBinderNames = []

def Lean.Expr.getNumHeadForalls :

Expr → Nat

Returns the number of leading ∀ binders of an expression. Ignores metadata.

Equations

(Lean.Expr.mdata data b).getNumHeadForalls = b.getNumHeadForalls
(Lean.Expr.forallE binderName binderType body binderInfo).getNumHeadForalls = body.getNumHeadForalls + 1
x✝.getNumHeadForalls = 0

def Lean.Expr.getAppFn :

Expr → Expr

If the given expression is a sequence of function applications f a₁ .. aₙ, return f. Otherwise return the input expression.

Equations

(fn.app arg).getAppFn = fn.getAppFn
x✝.getAppFn = x✝

def Lean.Expr.getAppFn' :

Expr → Expr

Similar to getAppFn, but skips mdata

Equations

(f.app arg).getAppFn' = f.getAppFn'
(Lean.Expr.mdata data a).getAppFn' = a.getAppFn'
x✝.getAppFn' = x✝

def Lean.Expr.isAppOf (e : Expr) (n : Name) :

Given f a₀ a₁ ... aₙ, returns true if f is a constant with name n.

Equations

e.isAppOf n = match e.getAppFn with | Lean.Expr.const c us => c == n | x => false

def Lean.Expr.isAppOfArity :

Expr → Name → Nat → Bool

Given f a₁ ... aᵢ, returns true if f is a constant with name n and has the correct number of arguments.

Equations

(Lean.Expr.const c us).isAppOfArity x✝ 0 = (c == x✝)
(f.app arg).isAppOfArity x✝ a.succ = f.isAppOfArity x✝ a
x✝².isAppOfArity x✝¹ x✝ = false

def Lean.Expr.isAppOfArity' :

Expr → Name → Nat → Bool

Similar to isAppOfArity but skips Expr.mdata.

def Lean.Expr.getAppNumArgs (e : Expr) :

Counts the number n of arguments for an expression f a₁ .. aₙ.

Equations

e.getAppNumArgs = Lean.Expr.getAppNumArgsAux✝ e 0

def Lean.Expr.getAppNumArgs' (e : Expr) :

Like getAppNumArgs but ignores metadata.

Equations

e.getAppNumArgs' = Lean.Expr.getAppNumArgs'.go e 0

def Lean.Expr.getAppNumArgs'.go :

Expr → Nat → Nat

Auxiliary definition for getAppNumArgs'.

Equations

Lean.Expr.getAppNumArgs'.go (Lean.Expr.mdata data b) x✝ = Lean.Expr.getAppNumArgs'.go b x✝
Lean.Expr.getAppNumArgs'.go (f.app arg) x✝ = Lean.Expr.getAppNumArgs'.go f (x✝ + 1)
Lean.Expr.getAppNumArgs'.go x✝¹ x✝ = x✝

def Lean.Expr.getBoundedAppFn (maxArgs : Nat) :

Expr → Expr

Like Lean.Expr.getAppFn but assumes the application has up to maxArgs arguments. If there are any more arguments than this, then they are returned by getAppFn as part of the function.

In particular, if the given expression is a sequence of function applications f a₁ .. aₙ, returns f a₁ .. aₖ where k is minimal such that n - k ≤ maxArgs.

Equations

Lean.Expr.getBoundedAppFn maxArgs'.succ (f.app arg) = Lean.Expr.getBoundedAppFn maxArgs' f
Lean.Expr.getBoundedAppFn x✝¹ x✝ = x✝

@[inline]

def Lean.Expr.getAppArgs (e : Expr) :

Given f a₁ a₂ ... aₙ, returns #[a₁, ..., aₙ]

Equations

e.getAppArgs = Lean.Expr.getAppArgsAux✝ e (mkArray e.getAppNumArgs (Lean.mkSort Lean.levelZero)) (e.getAppNumArgs - 1)

@[inline]

def Lean.Expr.getBoundedAppArgs (maxArgs : Nat) (e : Expr) :

Like Lean.Expr.getAppArgs but returns up to maxArgs arguments.

In particular, given f a₁ a₂ ... aₙ, returns #[aₖ₊₁, ..., aₙ] where k is minimal such that the size of this array is at most maxArgs.

Equations

Lean.Expr.getBoundedAppArgs maxArgs e = Lean.Expr.getBoundedAppArgsAux✝ e (mkArray (min maxArgs e.getAppNumArgs) (Lean.mkSort Lean.levelZero)) (min maxArgs e.getAppNumArgs)

@[inline]

def Lean.Expr.getAppRevArgs (e : Expr) :

Same as getAppArgs but reverse the output array.

Equations

e.getAppRevArgs = Lean.Expr.getAppRevArgsAux✝ e (Array.mkEmpty e.getAppNumArgs)

@[specialize #[]]

def Lean.Expr.withAppAux {α : Sort u_1} (k : Expr → Array Expr → α) :

Expr → Array Expr → Nat → α

Equations

Lean.Expr.withAppAux k (f.app a) x✝¹ x✝ = Lean.Expr.withAppAux k f (x✝¹.set! x✝ a) (x✝ - 1)
Lean.Expr.withAppAux k x✝² x✝¹ x✝ = k x✝² x✝¹

@[inline]

def Lean.Expr.withApp {α : Sort u_1} (e : Expr) (k : Expr → Array Expr → α) :

Given e = f a₁ a₂ ... aₙ, returns k f #[a₁, ..., aₙ].

Equations

e.withApp k = Lean.Expr.withAppAux k e (mkArray e.getAppNumArgs (Lean.mkSort Lean.levelZero)) (e.getAppNumArgs - 1)

def Lean.Expr.getAppFnArgs (e : Expr) :

Name × Array Expr

Return the function (name) and arguments of an application.

Equations

e.getAppFnArgs = e.withApp fun (e : Lean.Expr) (a : Array Lean.Expr) => (e.constName, a)

@[inline]

def Lean.Expr.getAppArgsN (e : Expr) (n : Nat) :

Given f a_1 ... a_n, returns #[a_1, ..., a_n]. Note that f may be an application. The resulting array has size n even if f.getAppNumArgs < n.

Equations

e.getAppArgsN n = Lean.Expr.getAppArgsN.loop n e (mkArray n (Lean.mkSort Lean.levelZero))

def Lean.Expr.getAppArgsN.loop :

Nat → Expr → Array Expr → Array Expr

Equations

Lean.Expr.getAppArgsN.loop 0 x✝¹ x✝ = x✝
Lean.Expr.getAppArgsN.loop i.succ (f.app a) x✝ = Lean.Expr.getAppArgsN.loop i f (x✝.set! i a)
Lean.Expr.getAppArgsN.loop x✝² x✝¹ x✝ = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.getAppArgsN.loop" 1190 27 "too few arguments at"

def Lean.Expr.stripArgsN (e : Expr) (n : Nat) :

Given e of the form f a_1 ... a_n, return f. If n is greater than the number of arguments, then return e.getAppFn.

def Lean.Expr.getAppPrefix (e : Expr) (n : Nat) :

Given e of the form f a_1 ... a_n ... a_m, return f a_1 ... a_n. If n is greater than the arity, then return e.

Equations

e.getAppPrefix n = e.stripArgsN (e.getAppNumArgs - n)

def Lean.Expr.traverseApp {M : Type → Type u_1} [Monad M] (f : Expr → M Expr) (e : Expr) :

M Expr

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 = e.withApp fun (fn : Lean.Expr) (args : Array Lean.Expr) => Lean.mkAppN <$> f fn <*> Array.mapM f args

@[inline]

def Lean.Expr.withAppRev {α : Sort u_1} (e : Expr) (k : Expr → Array Expr → α) :

Same as withApp but with arguments reversed.

Equations

e.withAppRev k = Lean.Expr.withAppRevAux✝ k e (Array.mkEmpty e.getAppNumArgs)

def Lean.Expr.getRevArgD :

Expr → Nat → Expr → Expr

Equations

(fn.app a).getRevArgD 0 x✝ = a
(f.app arg).getRevArgD i.succ x✝ = f.getRevArgD i x✝
x✝².getRevArgD x✝¹ x✝ = x✝

def Lean.Expr.getRevArg! :

Expr → Nat → Expr

Equations

(fn.app a).getRevArg! 0 = a
(f.app arg).getRevArg! i.succ = f.getRevArg! i
x✝¹.getRevArg! x✝ = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.getRevArg!" 1231 20 "invalid index"

def Lean.Expr.getRevArg!' :

Expr → Nat → Expr

Similar to getRevArg! but skips mdata

Equations

(Lean.Expr.mdata data a).getRevArg!' x✝ = a.getRevArg!' x✝
(fn.app a).getRevArg!' 0 = a
(f.app arg).getRevArg!' i.succ = f.getRevArg!' i
x✝¹.getRevArg!' x✝ = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.getRevArg!'" 1238 20 "invalid index"

@[inline]

def Lean.Expr.getArg! (e : Expr) (i : Nat) (n : Nat := e.getAppNumArgs) :

Given f a₀ a₁ ... aₙ, returns the ith argument or panics if out of bounds.

Equations

e.getArg! i n = e.getRevArg! (n - i - 1)

@[inline]

def Lean.Expr.getArg!' (e : Expr) (i : Nat) (n : Nat := e.getAppNumArgs) :

Similar to getArg!, but skips mdata

Equations

e.getArg!' i n = e.getRevArg!' (n - i - 1)

@[inline]

def Lean.Expr.getArgD (e : Expr) (i : Nat) (v₀ : Expr) (n : Nat := e.getAppNumArgs) :

Given f a₀ a₁ ... aₙ, returns the ith argument or returns v₀ if out of bounds.

Equations

e.getArgD i v₀ n = e.getRevArgD (n - i - 1) v₀

def Lean.Expr.hasLooseBVars (e : Expr) :

Return true if e contains any loose bound variables.

This is a constant time operation.

Equations

e.hasLooseBVars = decide (e.looseBVarRange > 0)

def Lean.Expr.isArrow (e : Expr) :

Return true if e is a non-dependent arrow. Remark: the following function assumes e does not have loose bound variables.

Equations

(Lean.Expr.forallE binderName binderType body binderInfo).isArrow = !body.hasLooseBVars
e.isArrow = false

@[extern lean_expr_has_loose_bvar]

opaque Lean.Expr.hasLooseBVar (e : Expr) (bvarIdx : Nat) :

Return true if e contains the specified loose bound variable with index bvarIdx.

This operation traverses the expression tree.

def Lean.Expr.hasLooseBVarInExplicitDomain (e : Expr) (bvarIdx : Nat) (considerRange : Bool) :

Returns true if e contains the loose bound variable bvarIdx in an explicit parameter, or in the range if considerRange == true. Additionally, if the bound variable appears in an implicit parameter, it transitively looks for that implicit parameter.

Equations

One or more equations did not get rendered due to their size.
e.hasLooseBVarInExplicitDomain bvarIdx considerRange = (considerRange && e.hasLooseBVar bvarIdx)

@[extern lean_expr_lower_loose_bvars]

opaque Lean.Expr.lowerLooseBVars (e : Expr) (s d : Nat) :

Lower the loose bound variables >= s in e by d. That is, a loose bound variable bvar i with i >= s is mapped to bvar (i-d).

Remark: if s < d, then the result is e.

@[extern lean_expr_lift_loose_bvars]

opaque Lean.Expr.liftLooseBVars (e : Expr) (s d : Nat) :

Lift loose bound variables >= s in e by d.

def Lean.Expr.inferImplicit (e : Expr) (numParams : Nat) (considerRange : Bool) :

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 binder annotations of structure projections.

Equations

One or more equations did not get rendered due to their size.
e.inferImplicit numParams considerRange = e

@[extern lean_expr_instantiate]

opaque Lean.Expr.instantiate (e : Expr) (subst : Array Expr) :

Instantiates the loose bound variables in e using the subst array, where a loose Expr.bvar i at "binding depth" d is instantiated with subst[i - d] if 0 <= i - d < subst.size, and otherwise it is replaced with Expr.bvar (i - subst.size); non-loose bound variables are not touched.

If we imagine all expressions as being able to refer to the infinite list of loose bound variables ..., 3, 2, 1, 0 in that order, then conceptually instantiate is instantiating the last n of these and reindexing the remaining ones. Warning: instantiate uses the de Bruijn indexing to index the subst array, which might be the reverse order from what you might expect. See also Lean.Expr.instantiateRev.

Terminology. The "binding depth" of a subexpression is the number of bound variables available to that subexpression by virtue of being in the bodies of Expr.forallE, Expr.lam, and Expr.letE expressions. A bound variable Expr.bvar i is "loose" if its de Bruijn index i is not less than its binding depth.)

About instantiation. Instantiation isn't mere substitution. When an expression from subst is being instantiated, its internal loose bound variables have their de Bruijn indices incremented by the binding depth of the replaced loose bound variable. This is necessary for the substituted expression to still refer to the correct binders after instantiation. Similarly, the reason loose bound variables not instantiated using subst have their de Bruijn indices decremented like Expr.bvar (i - subst.size) is that instantiate can be used to eliminate binding expressions internal to a larger expression, and this adjustment keeps these bound variables referring to the same binders.

@[extern lean_expr_instantiate1]

opaque Lean.Expr.instantiate1 (e subst : Expr) :

Instantiates loose bound variable 0 in e using the expression subst, where in particular a loose Expr.bvar i at binding depth d is instantiated with subst if i = d, and otherwise it is replaced with Expr.bvar (i - 1); non-loose bound variables are not touched.

If we imagine all expressions as being able to refer to the infinite list of loose bound variables ..., 3, 2, 1, 0 in that order, then conceptually instantiate1 is instantiating the last one of these and reindexing the remaining ones.

This function is equivalent to instantiate e #[subst], but it avoids allocating an array.

See the documentation for Lean.Expr.instantiate for a description of instantiation. In short, during instantiation the loose bound variables in subst have their own de Bruijn indices updated to account for the binding depth of the replaced loose bound variable.

@[extern lean_expr_instantiate_rev]

opaque Lean.Expr.instantiateRev (e : Expr) (subst : Array Expr) :

Instantiates the loose bound variables in e using the subst array. This is equivalent to Lean.Expr.instantiate e subst.reverse, but it avoids reversing the array. In particular, rather than instantiating Expr.bvar i with subst[i - d] it instantiates with subst[subst.size - 1 - (i - d)], where d is the binding depth.

This function instantiates with the "forwards" indexing scheme. For example, if e represents the expression fun x y => x + y, then instantiateRev e.bindingBody!.bindingBody! #[a, b] yields a + b. The instantiate function on the other hand would yield b + a, since de Bruijn indices count outwards.

@[extern lean_expr_instantiate_range]

opaque Lean.Expr.instantiateRange (e : Expr) (beginIdx endIdx : Nat) (subst : Array Expr) :

Similar to Lean.Expr.instantiate, but considers only the substitutions subst in the range [beginIdx, endIdx). Function panics if beginIdx <= endIdx <= subst.size does not hold.

This function is equivalent to instantiate e (subst.extract beginIdx endIdx), but it does not allocate a new array.

This instantiates with the "backwards" indexing scheme. See also Lean.Expr.instantiateRevRange, which instantiates with the "forwards" indexing scheme.

@[extern lean_expr_instantiate_rev_range]

opaque Lean.Expr.instantiateRevRange (e : Expr) (beginIdx endIdx : Nat) (subst : Array Expr) :

Similar to Lean.Expr.instantiateRev, but considers only the substitutions subst in the range [beginIdx, endIdx). Function panics if beginIdx <= endIdx <= subst.size does not hold.

This function is equivalent to instantiateRev e (subst.extract beginIdx endIdx), but it does not allocate a new array.

This instantiates with the "forwards" indexing scheme (see the docstring for Lean.Expr.instantiateRev for an example). See also Lean.Expr.instantiateRange, which instantiates with the "backwards" indexing scheme.

@[extern lean_expr_abstract]

opaque Lean.Expr.abstract (e : Expr) (xs : Array Expr) :

Replace free (or meta) variables xs with loose bound variables, with xs ordered from outermost to innermost de Bruijn index.

For example, e := f x y with xs := #[x, y] goes to f #1 #0, whereas e := f x y with xs := #[y, x] goes to f #0 #1.

@[extern lean_expr_abstract_range]

opaque Lean.Expr.abstractRange (e : Expr) (n : Nat) (xs : Array Expr) :

Similar to abstract, but consider only the first min n xs.size entries in xs.

def Lean.Expr.replaceFVar (e fvar v : Expr) :

Replace occurrences of the free variable fvar in e with v

Equations

e.replaceFVar fvar v = (e.abstract #[fvar]).instantiate1 v

def Lean.Expr.replaceFVarId (e : Expr) (fvarId : FVarId) (v : Expr) :

Replace occurrences of the free variable fvarId in e with v

Equations

e.replaceFVarId fvarId v = e.replaceFVar (Lean.mkFVar fvarId) v

def Lean.Expr.replaceFVars (e : Expr) (fvars vs : Array Expr) :

Replace occurrences of the free variables fvars in e with vs

Equations

e.replaceFVars fvars vs = (e.abstract fvars).instantiateRev vs

instance Lean.Expr.instToString :

ToString Expr

Equations

Lean.Expr.instToString = { toString := Lean.Expr.dbgToString }

def Lean.Expr.isAtomic :

Expr → Bool

Returns true when the expression does not have any sub-expressions.

Equations

(Lean.Expr.const declName us).isAtomic = true
(Lean.Expr.sort u).isAtomic = true
(Lean.Expr.bvar deBruijnIndex).isAtomic = true
(Lean.Expr.lit a).isAtomic = true
(Lean.Expr.mvar mvarId).isAtomic = true
(Lean.Expr.fvar fvarId).isAtomic = true
x✝.isAtomic = false

def Lean.mkDecIsTrue (pred proof : Expr) :

Equations

Lean.mkDecIsTrue pred proof = Lean.mkAppB (Lean.mkConst `Decidable.isTrue) pred proof

def Lean.mkDecIsFalse (pred proof : Expr) :

Equations

Lean.mkDecIsFalse pred proof = Lean.mkAppB (Lean.mkConst `Decidable.isFalse) pred proof

@[reducible, inline]

abbrev Lean.ExprMap (α : Type) :

Equations

Lean.ExprMap α = Std.HashMap Lean.Expr α

@[reducible, inline]

abbrev Lean.PersistentExprMap (α : Type) :

Equations

Lean.PersistentExprMap α = Lean.PHashMap Lean.Expr α

@[reducible, inline]

abbrev Lean.SExprMap (α : Type) :

Equations

Lean.SExprMap α = Lean.SMap Lean.Expr α

@[reducible, inline]

abbrev Lean.ExprSet :

Equations

Lean.ExprSet = Std.HashSet Lean.Expr

@[reducible, inline]

abbrev Lean.PersistentExprSet :

Equations

Lean.PersistentExprSet = Lean.PHashSet Lean.Expr

@[reducible, inline]

abbrev Lean.PExprSet :

Equations

Lean.PExprSet = Lean.PersistentExprSet

structure Lean.ExprStructEq :

Auxiliary type for forcing == to be structural equality for Expr

val : Expr

Instances For

instance Lean.instInhabitedExprStructEq :

Inhabited ExprStructEq

Equations

Lean.instInhabitedExprStructEq = { default := { val := default } }

instance Lean.instCoeExprExprStructEq :

Coe Expr ExprStructEq

Equations

Lean.instCoeExprExprStructEq = { coe := Lean.ExprStructEq.mk }

def Lean.ExprStructEq.beq :

ExprStructEq → ExprStructEq → Bool

Equations

{ val := e₁ }.beq { val := e₂ } = e₁.equal e₂

def Lean.ExprStructEq.hash :

ExprStructEq → UInt64

Equations

{ val := e }.hash = e.hash

instance Lean.ExprStructEq.instBEq :

BEq ExprStructEq

Equations

Lean.ExprStructEq.instBEq = { beq := Lean.ExprStructEq.beq }

instance Lean.ExprStructEq.instHashable :

Hashable ExprStructEq

Equations

Lean.ExprStructEq.instHashable = { hash := Lean.ExprStructEq.hash }

instance Lean.ExprStructEq.instToString :

ToString ExprStructEq

Equations

Lean.ExprStructEq.instToString = { toString := fun (e : Lean.ExprStructEq) => toString e.val }

@[reducible, inline]

abbrev Lean.ExprStructMap (α : Type) :

Equations

Lean.ExprStructMap α = Std.HashMap Lean.ExprStructEq α

@[reducible, inline]

abbrev Lean.PersistentExprStructMap (α : Type) :

Equations

Lean.PersistentExprStructMap α = Lean.PHashMap Lean.ExprStructEq α

def Lean.Expr.mkAppRevRange (f : Expr) (beginIdx endIdx : Nat) (revArgs : Array Expr) :

mkAppRevRange f b e args == mkAppRev f (revArgs.extract b e)

Equations

f.mkAppRevRange beginIdx endIdx revArgs = Lean.Expr.mkAppRevRangeAux✝ revArgs beginIdx f endIdx

def Lean.Expr.betaRev (f : Expr) (revArgs : Array Expr) (useZeta preserveMData : Bool := false) :

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 Suppose t is (fun x y => t x y) a b c d, then args := t.getAppRev is #[d, c, b, a], and betaRev (fun x y => t x y) #[d, c, b, a] is t 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

f.betaRev revArgs useZeta preserveMData = if (revArgs.size == 0) = true then f else let sz := revArgs.size; Lean.Expr.betaRev.go revArgs useZeta preserveMData sz f 0

partial def Lean.Expr.betaRev.go (revArgs : Array Expr) (useZeta preserveMData : Bool := false) (sz : Nat) (e : Expr) (i : Nat) :

def Lean.Expr.beta (f : Expr) (args : Array Expr) :

Apply the given arguments to f, beta-reducing if f is a lambda expression. See docstring for betaRev for examples.

Equations

f.beta args = f.betaRev args.reverse

def Lean.Expr.getNumHeadLambdas :

Expr → Nat

Count the number of lambdas at the head of the given expression.

Equations

(Lean.Expr.lam binderName binderType b binderInfo).getNumHeadLambdas = b.getNumHeadLambdas + 1
(Lean.Expr.mdata data b).getNumHeadLambdas = b.getNumHeadLambdas
x✝.getNumHeadLambdas = 0

def Lean.Expr.isHeadBetaTargetFn (useZeta : Bool) :

Expr → Bool

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 data b) = Lean.Expr.isHeadBetaTargetFn useZeta b
Lean.Expr.isHeadBetaTargetFn useZeta x✝ = false

def Lean.Expr.headBeta (e : Expr) :

(fun x => e) a ==> e[x/a].

Equations

e.headBeta = if Lean.Expr.isHeadBetaTargetFn false e.getAppFn = true then e.getAppFn.betaRev e.getAppRevArgs else e

def Lean.Expr.isHeadBetaTarget (e : Expr) (useZeta : Bool := false) :

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

e.isHeadBetaTarget useZeta = (e.isApp && Lean.Expr.isHeadBetaTargetFn useZeta e.getAppFn)

def Lean.Expr.etaExpanded? (e : Expr) :

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

e.etaExpanded? = Lean.Expr.etaExpandedAux✝ e 0

def Lean.Expr.etaExpandedStrict? :

Expr → Option Expr

Similar to etaExpanded?, but only succeeds if ₙ ≥ 1.

Equations

(Lean.Expr.lam binderName binderType body binderInfo).etaExpandedStrict? = Lean.Expr.etaExpandedAux✝ body 1
x✝.etaExpandedStrict? = none

def Lean.Expr.getOptParamDefault? (e : Expr) :

Return some e' if e is of the form optParam _ e'

Equations

e.getOptParamDefault? = if e.isAppOfArity `optParam 2 = true then some e.appArg! else none

def Lean.Expr.getAutoParamTactic? (e : Expr) :

Return some e' if e is of the form autoParam _ e'

Equations

e.getAutoParamTactic? = if e.isAppOfArity `autoParam 2 = true then some e.appArg! else none

@[export lean_is_out_param]

def Lean.Expr.isOutParam (e : Expr) :

Return true if e is of the form outParam _

Equations

e.isOutParam = e.isAppOfArity `outParam 1

def Lean.Expr.isSemiOutParam (e : Expr) :

Return true if e is of the form semiOutParam _

Equations

e.isSemiOutParam = e.isAppOfArity `semiOutParam 1

def Lean.Expr.isOptParam (e : Expr) :

Return true if e is of the form optParam _ _

Equations

e.isOptParam = e.isAppOfArity `optParam 2

def Lean.Expr.isAutoParam (e : Expr) :

Return true if e is of the form autoParam _ _

Equations

e.isAutoParam = e.isAppOfArity `autoParam 2

@[export lean_expr_consume_type_annotations]

partial def Lean.Expr.consumeTypeAnnotations (e : Expr) :

Remove outParam, optParam, and autoParam applications/annotations from e. Note that it does not remove nested annotations. Examples:

Given e of the form outParam (optParam Nat b), consumeTypeAnnotations e = b.
Given e of the form Nat → outParam (optParam Nat b), consumeTypeAnnotations e = e.

partial def Lean.Expr.cleanupAnnotations (e : Expr) :

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 form outParam (optParam Nat b), cleanupAnnotations e = b.
Given e of the form Nat → outParam (optParam Nat b), cleanupAnnotations e = e.

def Lean.Expr.appFnCleanup (e : Expr) (h : e.isApp = true) :

Similar to appFn, but also applies cleanupAnnotations to resulting function. This function is used compile the match_expr term.

Equations

(fn.app a).appFnCleanup x = fn.cleanupAnnotations

def Lean.Expr.isFalse (e : Expr) :

Equations

e.isFalse = e.cleanupAnnotations.isConstOf `False

def Lean.Expr.isTrue (e : Expr) :

Equations

e.isTrue = e.cleanupAnnotations.isConstOf `True

partial def Lean.Expr.getForallArity :

Expr → Nat

getForallArity type returns the arity of a forall-type. This function consumes nested annotations, and performs pending beta reductions. It does not use whnf. Examples:

If a is Nat, getForallArity a returns 0
If a is Nat → Bool, getForallArity a returns 1

def Lean.Expr.nat? (e : Expr) :

Option Nat

Checks if an expression is a "natural number numeral in normal form", i.e. of type Nat, and explicitly of the form OfNat.ofNat n where n matches .lit (.natVal n) for some literal natural number n. and if so returns n.

Equations

One or more equations did not get rendered due to their size.

def Lean.Expr.int? (e : Expr) :

Option Int

Checks if an expression is an "integer numeral in normal form", i.e. of type Nat or Int, and either a natural number numeral in normal form (as specified by nat?), or the negation of a positive natural number numeral in normal form, and if so returns the integer.

Equations

One or more equations did not get rendered due to their size.

@[inline]

def Lean.Expr.hasAnyFVar (e : Expr) (p : FVarId → Bool) :

Return true iff e contains a free variable which satisfies p.

Equations

e.hasAnyFVar p = Lean.Expr.hasAnyFVar.visit p e

@[specialize #[]]

def Lean.Expr.hasAnyFVar.visit (p : FVarId → Bool) (e : Expr) :

def Lean.Expr.containsFVar (e : Expr) (fvarId : FVarId) :

Return true if e contains the given free variable.

Equations

e.containsFVar fvarId = e.hasAnyFVar fun (x : Lean.FVarId) => x == 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.

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateApp!Impl]

def Lean.Expr.updateApp! (e newFn newArg : Expr) :

Equations

(fn.app arg).updateApp! newFn newArg = Lean.mkApp newFn newArg
e.updateApp! newFn newArg = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.updateApp!" 1747 15 "application expected"

@[inline]

def Lean.Expr.updateFVar! (e : Expr) (fvarIdNew : FVarId) :

Equations

(Lean.Expr.fvar fvarId).updateFVar! fvarIdNew = if (fvarId == fvarIdNew) = true then Lean.Expr.fvar fvarId else Lean.Expr.fvar fvarIdNew
e.updateFVar! fvarIdNew = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.updateFVar!" 1752 20 "fvar expected"

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateConst!Impl]

def Lean.Expr.updateConst! (e : Expr) (newLevels : List Level) :

Equations

(Lean.Expr.const declName us).updateConst! newLevels = Lean.mkConst declName newLevels
e.updateConst! newLevels = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.updateConst!" 1763 17 "constant expected"

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateSort!Impl]

def Lean.Expr.updateSort! (e : Expr) (newLevel : Level) :

Equations

(Lean.Expr.sort u).updateSort! newLevel = Lean.mkSort newLevel
e.updateSort! newLevel = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.updateSort!" 1774 14 "level expected"

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateMData!Impl]

def Lean.Expr.updateMData! (e newExpr : Expr) :

Equations

(Lean.Expr.mdata data expr).updateMData! newExpr = Lean.mkMData data newExpr
e.updateMData! newExpr = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.updateMData!" 1785 17 "mdata expected"

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateProj!Impl]

def Lean.Expr.updateProj! (e newExpr : Expr) :

Equations

(Lean.Expr.proj typeName idx struct).updateProj! newExpr = Lean.mkProj typeName idx newExpr
e.updateProj! newExpr = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.updateProj!" 1796 18 "proj expected"

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateForall!Impl]

def Lean.Expr.updateForall! (e : Expr) (newBinfo : BinderInfo) (newDomain newBody : Expr) :

Equations

(Lean.Expr.forallE binderName binderType body binderInfo).updateForall! newBinfo newDomain newBody = Lean.mkForall binderName newBinfo newDomain newBody
e.updateForall! newBinfo newDomain newBody = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.updateForall!" 1811 23 "forall expected"

@[inline]

def Lean.Expr.updateForallE! (e newDomain newBody : Expr) :

Equations

(Lean.Expr.forallE binderName binderType body binderInfo).updateForallE! newDomain newBody = (Lean.Expr.forallE binderName binderType body binderInfo).updateForall! binderInfo newDomain newBody
e.updateForallE! newDomain newBody = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.updateForallE!" 1816 24 "forall expected"

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateLambda!Impl]

def Lean.Expr.updateLambda! (e : Expr) (newBinfo : BinderInfo) (newDomain newBody : Expr) :

Equations

(Lean.Expr.lam binderName binderType body binderInfo).updateLambda! newBinfo newDomain newBody = Lean.mkLambda binderName newBinfo newDomain newBody
e.updateLambda! newBinfo newDomain newBody = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.updateLambda!" 1831 19 "lambda expected"

@[inline]

def Lean.Expr.updateLambdaE! (e newDomain newBody : Expr) :

Equations

(Lean.Expr.lam binderName binderType body binderInfo).updateLambdaE! newDomain newBody = (Lean.Expr.lam binderName binderType body binderInfo).updateLambda! binderInfo newDomain newBody
e.updateLambdaE! newDomain newBody = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.updateLambdaE!" 1836 20 "lambda expected"

@[implemented_by _private.Lean.Expr.0.Lean.Expr.updateLet!Impl]

def Lean.Expr.updateLet! (e newType newVal newBody : Expr) :

Equations

(Lean.Expr.letE declName type value body nonDep).updateLet! newType newVal newBody = Lean.Expr.letE declName newType newVal newBody nonDep
e.updateLet! newType newVal newBody = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.updateLet!" 1851 22 "let expression expected"

def Lean.Expr.updateFn :

Expr → Expr → Expr

Equations

(f.app a).updateFn x✝ = (f.app a).updateApp! (f.updateFn x✝) a
x✝¹.updateFn x✝ = x✝

partial def Lean.Expr.eta (e : Expr) :

Eta reduction. If e is of the form (fun x => f x), then return f.

def Lean.Expr.setOption {α : Type} (e : Expr) (optionName : Name) [KVMap.Value α] (val : α) :

Annotate e with the given option. The information is stored using metadata around e.

Equations

e.setOption optionName val = Lean.mkMData (Lean.KVMap.set Lean.MData.empty optionName val) e

def Lean.Expr.setPPExplicit (e : Expr) (flag : Bool) :

Annotate e with pp.explicit := flag The delaborator uses pp options.

Equations

e.setPPExplicit flag = e.setOption `pp.explicit flag

def Lean.Expr.setPPUniverses (e : Expr) (flag : Bool) :

Annotate e with pp.universes := flag The delaborator uses pp options.

Equations

e.setPPUniverses flag = e.setOption `pp.universes flag

def Lean.Expr.setPPPiBinderTypes (e : Expr) (flag : Bool) :

Annotate e with pp.piBinderTypes := flag The delaborator uses pp options.

Equations

e.setPPPiBinderTypes flag = e.setOption `pp.piBinderTypes flag

def Lean.Expr.setPPFunBinderTypes (e : Expr) (flag : Bool) :

Annotate e with pp.funBinderTypes := flag The delaborator uses pp options.

Equations

e.setPPFunBinderTypes flag = e.setOption `pp.funBinderTypes flag

def Lean.Expr.setPPNumericTypes (e : Expr) (flag : Bool) :

Annotate e with pp.explicit := flag The delaborator uses pp options.

Equations

e.setPPNumericTypes flag = e.setOption `pp.numericTypes flag

def Lean.Expr.setAppPPExplicit (e : Expr) :

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.
e.setAppPPExplicit = e

def Lean.Expr.setAppPPExplicitForExposingMVars (e : Expr) :

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.
e.setAppPPExplicitForExposingMVars = e

def Lean.Expr.isLetFun (e : Expr) :

Returns true if e is a let_fun expression, which is an expression of the form letFun v f. Ideally f is a lambda, but we do not require that here. Warning: if the let_fun is applied to additional arguments (such as in (let_fun f := id; id) 1), this function returns false.

Equations

e.isLetFun = e.isAppOfArity `letFun 4

def Lean.Expr.letFun? (e : Expr) :

Option (Name × Expr × Expr × Expr)

Recognizes a let_fun expression. For let_fun n : t := v; b, returns some (n, t, v, b), which are the first four arguments to Lean.Expr.letE. Warning: if the let_fun is applied to additional arguments (such as in (let_fun f := id; id) 1), this function returns none.

let_fun expressions are encoded as letFun v (fun (n : t) => b). They can be created using Lean.Meta.mkLetFun.

If in the encoding of let_fun the last argument to letFun is eta reduced, this returns Name.anonymous for the binder name.

Equations

(((((Lean.Expr.const `letFun us).app t).app _β).app v).app (Lean.Expr.lam binderName binderType body binderInfo)).letFun? = some (binderName, t, v, body)
(((((Lean.Expr.const `letFun us).app t).app _β).app v).app f).letFun? = some (Lean.Name.anonymous , t, v, f.app (Lean.Expr.bvar 0))
e.letFun? = none

def Lean.Expr.letFunAppArgs? (e : Expr) :

Option (Array Expr × Name × Expr × Expr × Expr)

Like Lean.Expr.letFun?, but handles the case when the let_fun expression is possibly applied to additional arguments. Returns those arguments in addition to the values returned by letFun?.

Equations

One or more equations did not get rendered due to their size.

@[specialize #[]]

def Lean.Expr.traverseChildren {M : Type → Type u_1} [Applicative M] (f : Expr → M Expr) :

Expr → M Expr

Maps f on each immediate child of the given expression.

Equations

Lean.Expr.traverseChildren f (Lean.Expr.forallE binderName d b binderInfo) = pure (Lean.Expr.forallE binderName d b binderInfo).updateForallE! <*> f d <*> f b
Lean.Expr.traverseChildren f (Lean.Expr.lam binderName d b binderInfo) = pure (Lean.Expr.lam binderName d b binderInfo).updateLambdaE! <*> f d <*> f b
Lean.Expr.traverseChildren f (Lean.Expr.mdata data b) = (Lean.Expr.mdata data b).updateMData! <$> f b
Lean.Expr.traverseChildren f (Lean.Expr.letE declName t v b nonDep) = pure (Lean.Expr.letE declName t v b nonDep).updateLet! <*> f t <*> f v <*> f b
Lean.Expr.traverseChildren f (l.app r) = pure (l.app r).updateApp! <*> f l <*> f r
Lean.Expr.traverseChildren f (Lean.Expr.proj typeName idx b) = (Lean.Expr.proj typeName idx b).updateProj! <$> f b
Lean.Expr.traverseChildren f x✝ = pure x✝

def Lean.Expr.foldlM {α : Type} {m : Type → Type u_1} [Monad m] (f : α → Expr → m α) (init : α) (e : Expr) :

m α

e.foldlM f a folds the monadic function f over the subterms of the expression e, with initial value a.

Equations

Lean.Expr.foldlM f init e = Prod.snd <$> (Lean.Expr.traverseChildren (fun (e' : Lean.Expr) (a : α) => Prod.mk e' <$> f a e') e).run init

def Lean.Expr.sizeWithoutSharing (e : Expr) :

Returns the size of e as a tree, i.e. nodes reachable via multiple paths are counted multiple times.

This is a naive implementation that visits shared subterms multiple times instead of caching their sizes. It is primarily meant for debugging.

Equations

(Lean.Expr.forallE binderName d b binderInfo).sizeWithoutSharing = 1 + d.sizeWithoutSharing + b.sizeWithoutSharing
(Lean.Expr.lam binderName d b binderInfo).sizeWithoutSharing = 1 + d.sizeWithoutSharing + b.sizeWithoutSharing
(Lean.Expr.mdata data e).sizeWithoutSharing = 1 + e.sizeWithoutSharing
(Lean.Expr.letE declName t v b nonDep).sizeWithoutSharing = 1 + t.sizeWithoutSharing + v.sizeWithoutSharing + b.sizeWithoutSharing
(f.app a).sizeWithoutSharing = 1 + f.sizeWithoutSharing + a.sizeWithoutSharing
(Lean.Expr.proj typeName idx e).sizeWithoutSharing = 1 + e.sizeWithoutSharing
(Lean.Expr.lit a).sizeWithoutSharing = 1
(Lean.Expr.const declName us).sizeWithoutSharing = 1
(Lean.Expr.sort u).sizeWithoutSharing = 1
(Lean.Expr.mvar mvarId).sizeWithoutSharing = 1
(Lean.Expr.fvar fvarId).sizeWithoutSharing = 1
(Lean.Expr.bvar deBruijnIndex).sizeWithoutSharing = 1

def Lean.mkAnnotation (kind : Name) (e : Expr) :

Annotate e with the given annotation name kind. It uses metadata to store the annotation.

Equations

Lean.mkAnnotation kind e = Lean.mkMData (Lean.KVMap.empty.insert kind (Lean.DataValue.ofBool true)) e

def Lean.annotation? (kind : Name) (e : Expr) :

Return some e' if e = mkAnnotation kind e'

Equations

Lean.annotation? kind (Lean.Expr.mdata data expr) = if (Lean.KVMap.size data == 1 && Lean.KVMap.getBool data kind) = true then some expr else none
Lean.annotation? kind e = none

def Lean.mkInaccessible (e : Expr) :

Auxiliary annotation used to mark terms marked with the "inaccessible" annotation .(t) and _ in patterns.

Equations

Lean.mkInaccessible e = Lean.mkAnnotation `_inaccessible e

def Lean.inaccessible? (e : Expr) :

Return some e' if e = mkInaccessible e'.

Equations

Lean.inaccessible? e = Lean.annotation? `_inaccessible e

def Lean.patternWithRef? (p : Expr) :

Option (Syntax × Expr)

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.
Lean.patternWithRef? p = none

def Lean.isPatternWithRef (p : Expr) :

Equations

Lean.isPatternWithRef p = (Lean.patternWithRef? p).isSome

def Lean.mkPatternWithRef (p : Expr) (stx : Syntax) :

Annotate the pattern p with stx. This is an auxiliary annotation for producing better hover information.

Equations

Lean.mkPatternWithRef p stx = if (Lean.patternWithRef? p).isSome = true then p else Lean.mkMData (Lean.KVMap.empty.insert Lean.patternRefAnnotationKey✝ (Lean.DataValue.ofSyntax stx)) p

def Lean.patternAnnotation? (e : Expr) :

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

def Lean.mkLHSGoalRaw (e : Expr) :

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 `_lhsGoal e

def Lean.isLHSGoal? (e : Expr) :

Return some lhs if e = mkLHSGoal e', where e' is of the form lhs = rhs.

Equations

Lean.isLHSGoal? e = match Lean.annotation? `_lhsGoal e with | none => none | some e => if e.isAppOfArity `Eq 3 = true then some e.appFn!.appArg! else none

def Lean.mkFreshFVarId {m : Type → Type} [Monad m] [MonadNameGenerator m] :

m FVarId

Polymorphic operation for generating unique/fresh free variable identifiers. It is available in any monad m that implements the interface MonadNameGenerator.

Equations

Lean.mkFreshFVarId = do let __do_lift ← Lean.mkFreshId pure { name := __do_lift }

def Lean.mkFreshMVarId {m : Type → Type} [Monad m] [MonadNameGenerator m] :

m MVarId

Polymorphic operation for generating unique/fresh metavariable identifiers. It is available in any monad m that implements the interface MonadNameGenerator.

Equations

Lean.mkFreshMVarId = do let __do_lift ← Lean.mkFreshId pure { name := __do_lift }