Lean.Expr

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

source

instance Lean.instInhabitedBinderInfo:

Inhabited Lean.BinderInfo

Equations

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

source

instance Lean.instBEqBinderInfo:

BEq Lean.BinderInfo

Equations

Lean.instBEqBinderInfo = { beq := [anonymous] }

source

instance Lean.instReprBinderInfo:

Repr Lean.BinderInfo

Equations

Lean.instReprBinderInfo = { reprPrec := [anonymous] }

source

def Lean.BinderInfo.hash:

Lean.BinderInfo → UInt64

Equations

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

source

def Lean.BinderInfo.isExplicit:

Lean.BinderInfo → Bool

Equations

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

source

instance Lean.instHashableBinderInfo:

Hashable Lean.BinderInfo

Equations

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

source

def Lean.BinderInfo.isInstImplicit:

Lean.BinderInfo → Bool

Equations

Lean.BinderInfo.isInstImplicit _fun_discr = match _fun_discr with | Lean.BinderInfo.instImplicit => true | x => false

source

def Lean.BinderInfo.isImplicit:

Lean.BinderInfo → Bool

Equations

Lean.BinderInfo.isImplicit _fun_discr = match _fun_discr with | Lean.BinderInfo.implicit => true | x => false

source

def Lean.BinderInfo.isStrictImplicit:

Lean.BinderInfo → Bool

Equations

Lean.BinderInfo.isStrictImplicit _fun_discr = match _fun_discr with | Lean.BinderInfo.strictImplicit => true | x => false

source

def Lean.BinderInfo.isAuxDecl:

Lean.BinderInfo → Bool

Equations

Lean.BinderInfo.isAuxDecl _fun_discr = match _fun_discr with | Lean.BinderInfo.auxDecl => true | x => false

source

@[inline]

abbrev Lean.MData:

Type

Expression metadata. Used with the Expr.mdata constructor.

Equations

Lean.MData = Lean.KVMap

source

@[inline]

abbrev Lean.MData.empty:

Lean.MData

Equations

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

source

def Lean.Expr.Data:

Type

Cached hash code, cached results, and other data for Expr. hash : 32-bits 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? nonDepLet : 1-bit -- internal flag, for tracking whether let x := v; b is equivalent to (fun x => b) v binderInfo : 3-bits -- encoding of BinderInfo approxDepth : 8-bits -- the approximate depth is used to minimize the number of hash collisions looseBVarRange : 16-bits

Equations

Lean.Expr.Data = UInt64

source

instance Lean.instInhabitedData_1:

Inhabited Lean.Expr.Data

Equations

Lean.instInhabitedData_1 = inferInstanceAs (Inhabited UInt64)

source

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

UInt64

Equations

Lean.Expr.Data.hash c = UInt32.toUInt64 (UInt64.toUInt32 c)

source

instance Lean.instBEqData_1:

BEq Lean.Expr.Data

Equations

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

source

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

UInt8

Equations

Lean.Expr.Data.approxDepth c = UInt64.toUInt8 (UInt64.land (UInt64.shiftRight c 40) 255)

source

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

UInt32

Equations

Lean.Expr.Data.looseBVarRange c = UInt64.toUInt32 (UInt64.shiftRight c 48)

source

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

Bool

Equations

Lean.Expr.Data.hasFVar c = (UInt64.land (UInt64.shiftRight c 32) 1 == 1)

source

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

Bool

Equations

Lean.Expr.Data.hasExprMVar c = (UInt64.land (UInt64.shiftRight c 33) 1 == 1)

source

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

Bool

Equations

Lean.Expr.Data.hasLevelMVar c = (UInt64.land (UInt64.shiftRight c 34) 1 == 1)

source

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

Bool

Equations

Lean.Expr.Data.hasLevelParam c = (UInt64.land (UInt64.shiftRight c 35) 1 == 1)

source

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

Bool

Equations

Lean.Expr.Data.nonDepLet c = (UInt64.land (UInt64.shiftRight c 36) 1 == 1)

source

@[extern c inline "(uint8_t)((#1 << 24) >> 61)"]

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

Lean.BinderInfo

Equations

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

source

@[extern c inline "(uint64_t)#1"]

def Lean.BinderInfo.toUInt64:

Lean.BinderInfo → UInt64

Equations

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

source

def Lean.Expr.mkData (h : UInt64) (looseBVarRange : optParam Nat 0) (approxDepth : optParam UInt32 0) (hasFVar : optParam Bool false) (hasExprMVar : optParam Bool false) (hasLevelMVar : optParam Bool false) (hasLevelParam : optParam Bool false) (bi : optParam Lean.BinderInfo Lean.BinderInfo.default) (nonDepLet : optParam Bool false) :

Lean.Expr.Data

Equations

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

source

@[inline]

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

Lean.Expr.Data

Optimized version of Expr.mkData for applications.

Equations

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

source

@[inline]

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

Lean.Expr.Data

Equations

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

source

@[inline]

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

Lean.Expr.Data

Equations

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

source

instance Lean.instReprData_1:

Repr Lean.Expr.Data

Equations

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

source

structure Lean.FVarId:

Type

name : Lean.Name

source

instance Lean.instInhabitedFVarId:

Inhabited Lean.FVarId

Equations

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

source

instance Lean.instBEqFVarId:

BEq Lean.FVarId

Equations

Lean.instBEqFVarId = { beq := [anonymous] }

source

instance Lean.instHashableFVarId:

Hashable Lean.FVarId

Equations

Lean.instHashableFVarId = { hash := [anonymous] }

source

instance Lean.instReprFVarId:

Repr Lean.FVarId

Equations

Lean.instReprFVarId = { reprPrec := fun n p => reprPrec n.name p }

source

def Lean.FVarIdSet:

Type

Equations

Lean.FVarIdSet = Std.RBTree Lean.FVarId fun a a_1 => Lean.Name.quickCmp a.name a_1.name

source

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

ForIn m Lean.FVarIdSet Lean.FVarId

Equations

Lean.instForInFVarIdSetFVarId = inferInstanceAs (ForIn m (Std.RBTree Lean.FVarId fun a a_1 => Lean.Name.quickCmp a.name a_1.name) Lean.FVarId)

source

def Lean.FVarIdHashSet:

Type

Equations

Lean.FVarIdHashSet = Std.HashSet Lean.FVarId

source

def Lean.FVarIdMap (α : Type) :

Type

Equations

Lean.FVarIdMap α = Std.RBMap Lean.FVarId α fun a a_1 => Lean.Name.quickCmp a.name a_1.name

source

instance Lean.instEmptyCollectionFVarIdMap {α : Type} :

EmptyCollection (Lean.FVarIdMap α)

Equations

Lean.instEmptyCollectionFVarIdMap = inferInstanceAs (EmptyCollection (Std.RBMap Lean.FVarId α fun a a_1 => Lean.Name.quickCmp a.name a_1.name))

source

instance Lean.instInhabitedFVarIdMap {α : Type} :

Inhabited (Lean.FVarIdMap α)

Equations

Lean.instInhabitedFVarIdMap = { default := ∅ }

source

inductive Lean.Expr:

Type

bvar: Nat → Lean.Expr.Data → Lean.Expr
fvar: Lean.FVarId → Lean.Expr.Data → Lean.Expr
mvar: Lean.MVarId → Lean.Expr.Data → Lean.Expr
sort: Lean.Level → Lean.Expr.Data → Lean.Expr
const: Lean.Name → List Lean.Level → Lean.Expr.Data → Lean.Expr
app: Lean.Expr → Lean.Expr → Lean.Expr.Data → Lean.Expr
lam: Lean.Name → Lean.Expr → Lean.Expr → Lean.Expr.Data → Lean.Expr
forallE: Lean.Name → Lean.Expr → Lean.Expr → Lean.Expr.Data → Lean.Expr
letE: Lean.Name → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr.Data → Lean.Expr
lit: Lean.Literal → Lean.Expr.Data → Lean.Expr
mdata: Lean.MData → Lean.Expr → Lean.Expr.Data → Lean.Expr
proj: Lean.Name → Nat → Lean.Expr → Lean.Expr.Data → Lean.Expr

source

instance Lean.instInhabitedExpr:

Inhabited Lean.Expr

Equations

Lean.instInhabitedExpr = { default := Lean.Expr.bvar default default }

source

instance Lean.instReprExpr:

Repr Lean.Expr

Equations

Lean.instReprExpr = { reprPrec := [anonymous] }

source

@[extern c inline "lean_ctor_get_uint64(#1, lean_ctor_num_objs(#1)*sizeof(void*))"]

def Lean.Expr.data:

Lean.Expr → Lean.Expr.Data

Equations

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

source

def Lean.Expr.ctorName:

Lean.Expr → String

Equations

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

source

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

UInt64

Equations

Lean.Expr.hash e = Lean.Expr.Data.hash (Lean.Expr.data e)

source

instance Lean.Expr.instHashableExpr:

Hashable Lean.Expr

Equations

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

source

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

Bool

Equations

Lean.Expr.hasFVar e = Lean.Expr.Data.hasFVar (Lean.Expr.data e)

source

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

Bool

Equations

Lean.Expr.hasExprMVar e = Lean.Expr.Data.hasExprMVar (Lean.Expr.data e)

source

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

Bool

Equations

Lean.Expr.hasLevelMVar e = Lean.Expr.Data.hasLevelMVar (Lean.Expr.data e)

source

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

Bool

Does the expression contain level or expression metavariables?

Equations

Lean.Expr.hasMVar e = let d := Lean.Expr.data e; Lean.Expr.Data.hasExprMVar d || Lean.Expr.Data.hasLevelMVar d

source

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

Bool

Equations

Lean.Expr.hasLevelParam e = Lean.Expr.Data.hasLevelParam (Lean.Expr.data e)

source

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

UInt32

Equations

Lean.Expr.approxDepth e = UInt8.toUInt32 (Lean.Expr.Data.approxDepth (Lean.Expr.data e))

source

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

Nat

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

Lean.Expr.looseBVarRange e = UInt32.toNat (Lean.Expr.Data.looseBVarRange (Lean.Expr.data e))

source

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

Lean.BinderInfo

Equations

Lean.Expr.binderInfo e = Lean.Expr.Data.binderInfo (Lean.Expr.data e)

source

@[export lean_expr_hash]

def Lean.Expr.hashEx:

Lean.Expr → UInt64

Equations

Lean.Expr.hashEx = hash

source

@[export lean_expr_has_fvar]

def Lean.Expr.hasFVarEx:

Lean.Expr → Bool

Equations

Lean.Expr.hasFVarEx = Lean.Expr.hasFVar

source

@[export lean_expr_has_expr_mvar]

def Lean.Expr.hasExprMVarEx:

Lean.Expr → Bool

Equations

Lean.Expr.hasExprMVarEx = Lean.Expr.hasExprMVar

source

@[export lean_expr_has_level_mvar]

def Lean.Expr.hasLevelMVarEx:

Lean.Expr → Bool

Equations

Lean.Expr.hasLevelMVarEx = Lean.Expr.hasLevelMVar

source

@[export lean_expr_has_mvar]

def Lean.Expr.hasMVarEx:

Lean.Expr → Bool

Equations

Lean.Expr.hasMVarEx = Lean.Expr.hasMVar

source

@[export lean_expr_has_level_param]

def Lean.Expr.hasLevelParamEx:

Lean.Expr → Bool

Equations

Lean.Expr.hasLevelParamEx = Lean.Expr.hasLevelParam

source

@[export lean_expr_loose_bvar_range]

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

UInt32

Equations

Lean.Expr.looseBVarRangeEx e = Lean.Expr.Data.looseBVarRange (Lean.Expr.data e)

source

@[export lean_expr_binder_info]

def Lean.Expr.binderInfoEx:

Lean.Expr → Lean.BinderInfo

Equations

Lean.Expr.binderInfoEx = Lean.Expr.binderInfo

source

def Lean.mkConst (n : Lean.Name) (lvls : optParam (List Lean.Level) []) :

Lean.Expr

Equations

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

source

def Lean.Literal.type:

Lean.Literal → Lean.Expr

Equations

Lean.Literal.type _fun_discr = match _fun_discr with | Lean.Literal.natVal val => Lean.mkConst `Nat | Lean.Literal.strVal val => Lean.mkConst `String

source

@[export lean_lit_type]

def Lean.Literal.typeEx:

Lean.Literal → Lean.Expr

Equations

Lean.Literal.typeEx = Lean.Literal.type

source

def Lean.mkBVar (idx : Nat) :

Lean.Expr

Equations

Lean.mkBVar idx = Lean.Expr.bvar idx (Lean.Expr.mkData (mixHash 7 (hash idx)) (idx + 1) 0 false false false false Lean.BinderInfo.default)

source

def Lean.mkSort (lvl : Lean.Level) :

Lean.Expr

Equations

Lean.mkSort lvl = Lean.Expr.sort lvl (Lean.Expr.mkData (mixHash 11 (hash lvl)) 0 0 false false (Lean.Level.hasMVar lvl) (Lean.Level.hasParam lvl) Lean.BinderInfo.default)

source

def Lean.mkFVar (fvarId : Lean.FVarId) :

Lean.Expr

Equations

Lean.mkFVar fvarId = Lean.Expr.fvar fvarId (Lean.Expr.mkData (mixHash 13 (hash fvarId)) 0 0 true false false false Lean.BinderInfo.default)

source

def Lean.mkMVar (fvarId : Lean.MVarId) :

Lean.Expr

Equations

Lean.mkMVar fvarId = Lean.Expr.mvar fvarId (Lean.Expr.mkData (mixHash 17 (hash fvarId)) 0 0 false true false false Lean.BinderInfo.default)

source

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

Lean.Expr

Equations

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

source

def Lean.mkProj (s : Lean.Name) (i : Nat) (e : Lean.Expr) :

Lean.Expr

Equations

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

source

def Lean.mkApp (f : Lean.Expr) (a : Lean.Expr) :

Lean.Expr

Equations

Lean.mkApp f a = Lean.Expr.app f a (Lean.Expr.mkAppData (Lean.Expr.data f) (Lean.Expr.data a))

source

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

Lean.Expr

Equations

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

source

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

Lean.Expr

Equations

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

source

def Lean.mkSimpleThunkType (type : Lean.Expr) :

Lean.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

source

def Lean.mkSimpleThunk (type : Lean.Expr) :

Lean.Expr

Return fun (_ : Unit), e

Equations

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

source

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

Lean.Expr

Equations

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

source

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

Lean.Expr

Equations

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

source

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

Lean.Expr

Equations

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

source

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

Lean.Expr

Equations

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

source

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

Lean.Expr

Equations

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

source

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

Lean.Expr

Equations

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

source

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

Lean.Expr

Equations

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

source

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

Lean.Expr

Equations

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

source

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

Lean.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₄

source

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

Lean.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₅

source

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

Lean.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₆

source

def Lean.mkLit (l : Lean.Literal) :

Lean.Expr

Equations

Lean.mkLit l = Lean.Expr.lit l (Lean.Expr.mkData (mixHash 3 (hash l)) 0 0 false false false false Lean.BinderInfo.default)

source

def Lean.mkRawNatLit (n : Nat) :

Lean.Expr

Equations

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

source

def Lean.mkNatLit (n : Nat) :

Lean.Expr

Equations

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

source

def Lean.mkStrLit (s : String) :

Lean.Expr

Equations

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

source

@[export lean_expr_mk_bvar]

def Lean.mkBVarEx:

Nat → Lean.Expr

Equations

Lean.mkBVarEx = Lean.mkBVar

source

@[export lean_expr_mk_fvar]

def Lean.mkFVarEx:

Lean.FVarId → Lean.Expr

Equations

Lean.mkFVarEx = Lean.mkFVar

source

@[export lean_expr_mk_mvar]

def Lean.mkMVarEx:

Lean.MVarId → Lean.Expr

Equations

Lean.mkMVarEx = Lean.mkMVar

source

@[export lean_expr_mk_sort]

def Lean.mkSortEx:

Lean.Level → Lean.Expr

Equations

Lean.mkSortEx = Lean.mkSort

source

@[export lean_expr_mk_const]

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

Lean.Expr

Equations

Lean.mkConstEx c lvls = Lean.mkConst c lvls

source

@[export lean_expr_mk_app]

def Lean.mkAppEx:

Lean.Expr → Lean.Expr → Lean.Expr

Equations

Lean.mkAppEx = Lean.mkApp

source

@[export lean_expr_mk_lambda]

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

Lean.Expr

Equations

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

source

@[export lean_expr_mk_forall]

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

Lean.Expr

Equations

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

source

@[export lean_expr_mk_let]

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

Lean.Expr

Equations

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

source

@[export lean_expr_mk_lit]

def Lean.mkLitEx:

Lean.Literal → Lean.Expr

Equations

Lean.mkLitEx = Lean.mkLit

source

@[export lean_expr_mk_mdata]

def Lean.mkMDataEx:

Lean.MData → Lean.Expr → Lean.Expr

Equations

Lean.mkMDataEx = Lean.mkMData

source

@[export lean_expr_mk_proj]

def Lean.mkProjEx:

Lean.Name → Nat → Lean.Expr → Lean.Expr

Equations

Lean.mkProjEx = Lean.mkProj

source

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

Lean.Expr

mkAppN f #[a₀, ..., aₙ] ==> f a₀ a₁ .. aₙ

Equations

Lean.mkAppN f args = Array.foldl Lean.mkApp f args 0 (Array.size args)

source

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

Lean.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

source

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

Lean.Expr

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)

source

@[extern lean_expr_dbg_to_string]

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

String

source

@[extern lean_expr_quick_lt]

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

Bool

source

@[extern lean_expr_lt]

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

Bool

source

@[extern lean_expr_eqv]

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

Bool

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

source

instance Lean.Expr.instBEqExpr:

BEq Lean.Expr

Equations

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

source

unsafe def Lean.Expr.ptrEq (a : Lean.Expr) (b : Lean.Expr) :

Bool

Equations

Lean.Expr.ptrEq a b = (ptrAddrUnsafe a == ptrAddrUnsafe b)

source

@[extern lean_expr_equal]

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

Bool

source

def Lean.Expr.isSort:

Lean.Expr → Bool

Equations

Lean.Expr.isSort _fun_discr = match _fun_discr with | Lean.Expr.sort a a_1 => true | x => false

source

def Lean.Expr.isType:

Lean.Expr → Bool

Equations

Lean.Expr.isType _fun_discr = match _fun_discr with | Lean.Expr.sort (Lean.Level.succ a a_1) a_2 => true | x => false

source

def Lean.Expr.isProp:

Lean.Expr → Bool

Equations

Lean.Expr.isProp _fun_discr = match _fun_discr with | Lean.Expr.sort (Lean.Level.zero a) a_1 => true | x => false

source

def Lean.Expr.isBVar:

Lean.Expr → Bool

Equations

Lean.Expr.isBVar _fun_discr = match _fun_discr with | Lean.Expr.bvar a a_1 => true | x => false

source

def Lean.Expr.isMVar:

Lean.Expr → Bool

Equations

Lean.Expr.isMVar _fun_discr = match _fun_discr with | Lean.Expr.mvar a a_1 => true | x => false

source

def Lean.Expr.isFVar:

Lean.Expr → Bool

Equations

Lean.Expr.isFVar _fun_discr = match _fun_discr with | Lean.Expr.fvar a a_1 => true | x => false

source

def Lean.Expr.isApp:

Lean.Expr → Bool

Equations

Lean.Expr.isApp _fun_discr = match _fun_discr with | Lean.Expr.app a a_1 a_2 => true | x => false

source

def Lean.Expr.isProj:

Lean.Expr → Bool

Equations

Lean.Expr.isProj _fun_discr = match _fun_discr with | Lean.Expr.proj a a_1 a_2 a_3 => true | x => false

source

def Lean.Expr.isConst:

Lean.Expr → Bool

Equations

Lean.Expr.isConst _fun_discr = match _fun_discr with | Lean.Expr.const a a_1 a_2 => true | x => false

source

def Lean.Expr.isConstOf:

Lean.Expr → Lean.Name → Bool

Equations

Lean.Expr.isConstOf _fun_discr _fun_discr = match _fun_discr, _fun_discr with | Lean.Expr.const n a a_1, m => n == m | x, x_1 => false

source

def Lean.Expr.isForall:

Lean.Expr → Bool

Equations

Lean.Expr.isForall _fun_discr = match _fun_discr with | Lean.Expr.forallE a a_1 a_2 a_3 => true | x => false

source

def Lean.Expr.isLambda:

Lean.Expr → Bool

Equations

Lean.Expr.isLambda _fun_discr = match _fun_discr with | Lean.Expr.lam a a_1 a_2 a_3 => true | x => false

source

def Lean.Expr.isBinding:

Lean.Expr → Bool

Equations

Lean.Expr.isBinding _fun_discr = match _fun_discr with | Lean.Expr.lam a a_1 a_2 a_3 => true | Lean.Expr.forallE a a_1 a_2 a_3 => true | x => false

source

def Lean.Expr.isLet:

Lean.Expr → Bool

Equations

Lean.Expr.isLet _fun_discr = match _fun_discr with | Lean.Expr.letE a a_1 a_2 a_3 a_4 => true | x => false

source

def Lean.Expr.isMData:

Lean.Expr → Bool

Equations

Lean.Expr.isMData _fun_discr = match _fun_discr with | Lean.Expr.mdata a a_1 a_2 => true | x => false

source

def Lean.Expr.isLit:

Lean.Expr → Bool

Equations

Lean.Expr.isLit _fun_discr = match _fun_discr with | Lean.Expr.lit a a_1 => true | x => false

source

def Lean.Expr.getForallBody:

Lean.Expr → Lean.Expr

Equations

Lean.Expr.getForallBody (Lean.Expr.forallE a a_1 a_2 a_3) = Lean.Expr.getForallBody a_2
Lean.Expr.getForallBody _fun_discr = _fun_discr

source

def Lean.Expr.getAppFn:

Lean.Expr → Lean.Expr

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 a a_1 a_2) = Lean.Expr.getAppFn a
Lean.Expr.getAppFn _fun_discr = _fun_discr

source

def Lean.Expr.getAppNumArgsAux:

Lean.Expr → Nat → Nat

Equations

Lean.Expr.getAppNumArgsAux (Lean.Expr.app f a a_1) _fun_discr = Lean.Expr.getAppNumArgsAux f (_fun_discr + 1)
Lean.Expr.getAppNumArgsAux _fun_discr _fun_discr = _fun_discr

source

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

Nat

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

Equations

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

source

@[inline]

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

Array Lean.Expr

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)

source

@[inline]

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

Array Lean.Expr

Same as getAppArgs but reverse the output array.

Equations

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

source

@[specialize]

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

Lean.Expr → Array Lean.Expr → Nat → α

Equations

Lean.Expr.withAppAux k (Lean.Expr.app f a a_1) _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

source

@[inline]

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

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)

source

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

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

source

@[inline]

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

Same as withApp but with arguments reversed.

Equations

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

source

def Lean.Expr.getRevArgD:

Lean.Expr → Nat → Lean.Expr → Lean.Expr

Equations

Lean.Expr.getRevArgD (Lean.Expr.app a a_1 a_2) 0 _fun_discr = a_1
Lean.Expr.getRevArgD (Lean.Expr.app f a a_1) (Nat.succ i) _fun_discr = Lean.Expr.getRevArgD f i _fun_discr
Lean.Expr.getRevArgD _fun_discr _fun_discr _fun_discr = _fun_discr

source

def Lean.Expr.getRevArg!:

Lean.Expr → Nat → Lean.Expr

Equations

Lean.Expr.getRevArg! (Lean.Expr.app a a_1 a_2) 0 = a_1
Lean.Expr.getRevArg! (Lean.Expr.app f a a_1) (Nat.succ i) = Lean.Expr.getRevArg! f i
Lean.Expr.getRevArg! _fun_discr _fun_discr = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.getRevArg!" 622 22 "invalid index"

source

@[inline]

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

Lean.Expr

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

Equations

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

source

@[inline]

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

Lean.Expr

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

Equations

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

source

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

Bool

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 a a_1 => c == n | x => false

source

def Lean.Expr.isAppOfArity:

Lean.Expr → Lean.Name → Nat → Bool

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

source

def Lean.Expr.isAppOfArity':

Lean.Expr → Lean.Name → Nat → Bool

Similar to isAppOfArity but skips Expr.mdata.

source

def Lean.Expr.appFn!:

Lean.Expr → Lean.Expr

Equations

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

source

def Lean.Expr.appArg!:

Lean.Expr → Lean.Expr

Equations

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

source

def Lean.Expr.appFn!':

Lean.Expr → Lean.Expr

Equations

Lean.Expr.appFn!' (Lean.Expr.mdata a b a_1) = Lean.Expr.appFn!' b
Lean.Expr.appFn!' (Lean.Expr.app f a a_1) = f
Lean.Expr.appFn!' _fun_discr = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appFn!'" 663 19 "application expected"

source

def Lean.Expr.appArg!':

Lean.Expr → Lean.Expr

Equations

Lean.Expr.appArg!' (Lean.Expr.mdata a b a_1) = Lean.Expr.appArg!' b
Lean.Expr.appArg!' (Lean.Expr.app f a a_1) = a
Lean.Expr.appArg!' _fun_discr = panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appArg!'" 668 19 "application expected"

source

def Lean.Expr.sortLevel!:

Lean.Expr → Lean.Level

Equations

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

source

def Lean.Expr.litValue!:

Lean.Expr → Lean.Literal

Equations

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

source

def Lean.Expr.isNatLit:

Lean.Expr → Bool

Equations

Lean.Expr.isNatLit _fun_discr = match _fun_discr with | Lean.Expr.lit (Lean.Literal.natVal val) a => true | x => false

source

def Lean.Expr.natLit?:

Lean.Expr → Option Nat

Equations

Lean.Expr.natLit? _fun_discr = match _fun_discr with | Lean.Expr.lit (Lean.Literal.natVal v) a => some v | x => none

source

def Lean.Expr.isStringLit:

Lean.Expr → Bool

Equations

Lean.Expr.isStringLit _fun_discr = match _fun_discr with | Lean.Expr.lit (Lean.Literal.strVal val) a => true | x => false

source

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

Bool

Equations

Lean.Expr.isCharLit e = (Lean.Expr.isAppOfArity e `Char.ofNat 1 && Lean.Expr.isNatLit (Lean.Expr.appArg! e))

source

def Lean.Expr.constName!:

Lean.Expr → Lean.Name

Equations

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

source

def Lean.Expr.constName?:

Lean.Expr → Option Lean.Name

Equations

Lean.Expr.constName? _fun_discr = match _fun_discr with | Lean.Expr.const n a a_1 => some n | x => none

source

def Lean.Expr.constLevels!:

Lean.Expr → List Lean.Level

Equations

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

source

def Lean.Expr.bvarIdx!:

Lean.Expr → Nat

Equations

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

source

def Lean.Expr.fvarId!:

Lean.Expr → Lean.FVarId

Equations

Lean.Expr.fvarId! _fun_discr = match _fun_discr with | Lean.Expr.fvar n a => n | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.fvarId!" 711 16 "fvar expected"

source

def Lean.Expr.mvarId!:

Lean.Expr → Lean.MVarId

Equations

Lean.Expr.mvarId! _fun_discr = match _fun_discr with | Lean.Expr.mvar n a => n | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.mvarId!" 715 16 "mvar expected"

source

def Lean.Expr.bindingName!:

Lean.Expr → Lean.Name

Equations

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

source

def Lean.Expr.bindingDomain!:

Lean.Expr → Lean.Expr

Equations

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

source

def Lean.Expr.bindingBody!:

Lean.Expr → Lean.Expr

Equations

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

source

def Lean.Expr.bindingInfo!:

Lean.Expr → Lean.BinderInfo

Equations

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

source

def Lean.Expr.letName!:

Lean.Expr → Lean.Name

Equations

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

source

def Lean.Expr.letType!:

Lean.Expr → Lean.Expr

Equations

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

source

def Lean.Expr.letValue!:

Lean.Expr → Lean.Expr

Equations

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

source

def Lean.Expr.letBody!:

Lean.Expr → Lean.Expr

Equations

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

source

def Lean.Expr.consumeMData:

Lean.Expr → Lean.Expr

Equations

Lean.Expr.consumeMData (Lean.Expr.mdata a a_1 a_2) = Lean.Expr.consumeMData a_1
Lean.Expr.consumeMData _fun_discr = _fun_discr

source

def Lean.Expr.mdataExpr!:

Lean.Expr → Lean.Expr

Equations

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

source

def Lean.Expr.projExpr!:

Lean.Expr → Lean.Expr

Equations

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

source

def Lean.Expr.projIdx!:

Lean.Expr → Nat

Equations

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

source

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

Bool

Equations

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

source

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

Bool

Equations

Lean.Expr.isArrow e = match e with | Lean.Expr.forallE a a_1 b a_2 => !Lean.Expr.hasLooseBVars b | x => false

source

@[extern lean_expr_has_loose_bvar]

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

Bool

source

def Lean.Expr.hasLooseBVarInExplicitDomain:

Lean.Expr → Nat → Bool → Bool

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)

source

@[extern lean_expr_lower_loose_bvars]

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

Lean.Expr

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

Remark: if s < d, then result is e

source

@[extern lean_expr_lift_loose_bvars]

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

Lean.Expr

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

source

def Lean.Expr.inferImplicit:

Lean.Expr → Nat → Bool → Lean.Expr

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.

source

@[extern lean_expr_instantiate]

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

Lean.Expr

Instantiate the loose bound variables in e using subst. That is, a loose Expr.bvar i is replaced with subst[i].

source

@[extern lean_expr_instantiate1]

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

Lean.Expr

source

@[extern lean_expr_instantiate_rev]

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

Lean.Expr

Similar to instantiate, but Expr.bvar i is replaced with subst[subst.size - i - 1]

source

@[extern lean_expr_instantiate_range]

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

Lean.Expr

Similar to instantiate, but consider only the variables xs in the range [beginIdx, endIdx). Function panics if beginIdx <= endIdx <= xs.size does not hold.

source

@[extern lean_expr_instantiate_rev_range]

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

Lean.Expr

Similar to instantiateRev, but consider only the variables xs in the range [beginIdx, endIdx). Function panics if beginIdx <= endIdx <= xs.size does not hold.

source

@[extern lean_expr_abstract]

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

Lean.Expr

Replace free (or meta) variables xs with loose bound variables.

source

@[extern lean_expr_abstract_range]

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

Lean.Expr

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

source

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

Lean.Expr

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

source

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

Lean.Expr

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

source

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

Lean.Expr

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

source

instance Lean.Expr.instToStringExpr:

ToString Lean.Expr

Equations

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

source

def Lean.Expr.isAtomic:

Lean.Expr → Bool

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

Equations

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

source

def Lean.mkDecIsTrue (pred : Lean.Expr) (proof : Lean.Expr) :

Lean.Expr

Equations

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

source

def Lean.mkDecIsFalse (pred : Lean.Expr) (proof : Lean.Expr) :

Lean.Expr

Equations

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

source

@[inline]

abbrev Lean.ExprMap (α : Type) :

Type

Equations

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

source

@[inline]

abbrev Lean.PersistentExprMap (α : Type) :

Type

Equations

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

source

@[inline]

abbrev Lean.ExprSet:

Type

Equations

Lean.ExprSet = Std.HashSet Lean.Expr

source

@[inline]

abbrev Lean.PersistentExprSet:

Type

Equations

Lean.PersistentExprSet = Std.PHashSet Lean.Expr

source

@[inline]

abbrev Lean.PExprSet:

Type

Equations

Lean.PExprSet = Lean.PersistentExprSet

source

structure Lean.ExprStructEq:

Type

val : Lean.Expr

source

instance Lean.instInhabitedExprStructEq:

Inhabited Lean.ExprStructEq

Equations

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

source

instance Lean.instCoeExprExprStructEq:

Coe Lean.Expr Lean.ExprStructEq

Equations

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

source

def Lean.ExprStructEq.beq:

Lean.ExprStructEq → Lean.ExprStructEq → Bool

Equations

Lean.ExprStructEq.beq _fun_discr _fun_discr = match _fun_discr, _fun_discr with | { val := e₁ }, { val := e₂ } => Lean.Expr.equal e₁ e₂

source

def Lean.ExprStructEq.hash:

Lean.ExprStructEq → UInt64

Equations

Lean.ExprStructEq.hash _fun_discr = match _fun_discr with | { val := e } => Lean.Expr.hash e

source

instance Lean.ExprStructEq.instBEqExprStructEq:

BEq Lean.ExprStructEq

Equations

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

source

instance Lean.ExprStructEq.instHashableExprStructEq:

Hashable Lean.ExprStructEq

Equations

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

source

instance Lean.ExprStructEq.instToStringExprStructEq:

ToString Lean.ExprStructEq

Equations

Lean.ExprStructEq.instToStringExprStructEq = { toString := fun e => toString e.val }

source

@[inline]

abbrev Lean.ExprStructMap (α : Type) :

Type

Equations

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

source

@[inline]

abbrev Lean.PersistentExprStructMap (α : Type) :

Type

Equations

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

source

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

Lean.Expr

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

source

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

Lean.Expr

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

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

source

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

Lean.Expr

source

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

Lean.Expr

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

source

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

Lean.Expr → Bool

source

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

Lean.Expr

(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

source

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

Bool

Equations

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

source

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

Option Lean.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

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

source

def Lean.Expr.etaExpandedStrict?:

Lean.Expr → Option Lean.Expr

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

Equations

Lean.Expr.etaExpandedStrict? _fun_discr = match _fun_discr with | Lean.Expr.lam a a_1 b a_2 => Lean.Expr.etaExpandedAux b 1 | x => none

source

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

Option Lean.Expr

Equations

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

source

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

Option Lean.Expr

Equations

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

source

@[export lean_is_out_param]

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

Bool

Equations

Lean.Expr.isOutParam e = Lean.Expr.isAppOfArity e `outParam 1

source

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

Bool

Equations

Lean.Expr.isOptParam e = Lean.Expr.isAppOfArity e `optParam 2

source

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

Bool

Equations

Lean.Expr.isAutoParam e = Lean.Expr.isAppOfArity e `autoParam 2

source

@[export lean_expr_consume_type_annotations]

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

Lean.Expr

source

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

Lean.Expr

source

@[inline]

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

Bool

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

Equations

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

source

@[specialize]

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

Bool

source

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

Bool

Equations

Lean.Expr.containsFVar e fvarId = Lean.Expr.hasAnyFVar e fun a => a == fvarId

source

@[extern lean_expr_update_app]

def Lean.Expr.updateApp (e : Lean.Expr) (newFn : Lean.Expr) (newArg : Lean.Expr) (h : Lean.Expr.isApp e = true) :

Lean.Expr

Equations

Lean.Expr.updateApp e newFn newArg h = Lean.mkApp newFn newArg

source

@[inline]

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

Lean.Expr

Equations

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

source

@[extern lean_expr_update_const]

def Lean.Expr.updateConst (e : Lean.Expr) (newLevels : List Lean.Level) (h : Lean.Expr.isConst e = true) :

Lean.Expr

Equations

Lean.Expr.updateConst e newLevels h = Lean.mkConst (Lean.Expr.constName! e) newLevels

source

@[inline]

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

Lean.Expr

Equations

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

source

@[extern lean_expr_update_sort]

def Lean.Expr.updateSort (e : Lean.Expr) (newLevel : Lean.Level) (h : Lean.Expr.isSort e = true) :

Lean.Expr

Equations

Lean.Expr.updateSort e newLevel h = Lean.mkSort newLevel

source

@[inline]

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

Lean.Expr

Equations

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

source

@[extern lean_expr_update_proj]

def Lean.Expr.updateProj (e : Lean.Expr) (newExpr : Lean.Expr) (h : Lean.Expr.isProj e = true) :

Lean.Expr

Equations

Lean.Expr.updateProj e newExpr h = match e, h with | Lean.Expr.proj s i a a_1, h => Lean.mkProj s i newExpr | x, h => e

source

@[extern lean_expr_update_mdata]

def Lean.Expr.updateMData (e : Lean.Expr) (newExpr : Lean.Expr) (h : Lean.Expr.isMData e = true) :

Lean.Expr

Equations

Lean.Expr.updateMData e newExpr h = match e, h with | Lean.Expr.mdata d a a_1, h => Lean.mkMData d newExpr | x, h => e

source

@[inline]

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

Lean.Expr

Equations

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

source

@[inline]

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

Lean.Expr

Equations

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

source

@[extern lean_expr_update_forall]

def Lean.Expr.updateForall (e : Lean.Expr) (newBinfo : Lean.BinderInfo) (newDomain : Lean.Expr) (newBody : Lean.Expr) (h : Lean.Expr.isForall e = true) :

Lean.Expr

Equations

Lean.Expr.updateForall e newBinfo newDomain newBody h = Lean.mkForall (Lean.Expr.bindingName! e) newBinfo newDomain newBody

source

@[inline]

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

Lean.Expr

Equations

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

source

@[inline]

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

Lean.Expr

Equations

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

source

@[extern lean_expr_update_lambda]

def Lean.Expr.updateLambda (e : Lean.Expr) (newBinfo : Lean.BinderInfo) (newDomain : Lean.Expr) (newBody : Lean.Expr) (h : Lean.Expr.isLambda e = true) :

Lean.Expr

Equations

Lean.Expr.updateLambda e newBinfo newDomain newBody h = Lean.mkLambda (Lean.Expr.bindingName! e) newBinfo newDomain newBody

source

@[inline]

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

Lean.Expr

Equations

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

source

@[inline]

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

Lean.Expr

Equations

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

source

@[extern lean_expr_update_let]

def Lean.Expr.updateLet (e : Lean.Expr) (newType : Lean.Expr) (newVal : Lean.Expr) (newBody : Lean.Expr) (h : Lean.Expr.isLet e = true) :

Lean.Expr

Equations

Lean.Expr.updateLet e newType newVal newBody h = Lean.mkLet (Lean.Expr.letName! e) newType newVal newBody

source

@[inline]

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

Lean.Expr

Equations

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

source

def Lean.Expr.updateFn:

Lean.Expr → Lean.Expr → Lean.Expr

Equations

Lean.Expr.updateFn (Lean.Expr.app f a a_1) _fun_discr = Lean.Expr.updateApp! (Lean.Expr.app f a a_1) (Lean.Expr.updateFn f _fun_discr) a
Lean.Expr.updateFn _fun_discr _fun_discr = _fun_discr

source

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

Lean.Expr

source

@[inline]

def Lean.Expr.instantiateLevelParamsCore (s : Lean.Name → Option Lean.Level) (e : Lean.Expr) :

Lean.Expr

Equations

Lean.Expr.instantiateLevelParamsCore s e = Lean.Expr.instantiateLevelParamsCore.visit s e

source

@[specialize]

def Lean.Expr.instantiateLevelParamsCore.visit (s : Lean.Name → Option Lean.Level) (e : Lean.Expr) :

Lean.Expr

source

def Lean.Expr.instantiateLevelParams (e : Lean.Expr) (paramNames : List Lean.Name) (lvls : List Lean.Level) :

Lean.Expr

Equations

Lean.Expr.instantiateLevelParams e paramNames lvls = Lean.Expr.instantiateLevelParamsCore (Lean.Expr.getParamSubst paramNames lvls) e

source

def Lean.Expr.instantiateLevelParamsArray (e : Lean.Expr) (paramNames : Array Lean.Name) (lvls : Array Lean.Level) :

Lean.Expr

Equations

Lean.Expr.instantiateLevelParamsArray e paramNames lvls = Lean.Expr.instantiateLevelParamsCore (fun p => Lean.Expr.getParamSubstArray paramNames lvls p 0) e

source

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

Lean.Expr

Annotate e with the given option.

Equations

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

source

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

Lean.Expr

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

Equations

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

source

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

Lean.Expr

Equations

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

source

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

Lean.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.

source

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

Lean.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.

source

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

Lean.Expr

Equations

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

source

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

Option Lean.Expr

Equations

Lean.annotation? kind e = match e with | Lean.Expr.mdata d b a => if (Lean.KVMap.size d == 1 && Lean.KVMap.getBool d kind) = true then some b else none | x => none

source

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

Lean.Expr

Equations

Lean.mkLetFunAnnotation e = Lean.mkAnnotation `let_fun e

source

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

Option Lean.Expr

Equations

Lean.letFunAnnotation? e = Lean.annotation? `let_fun e

source

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

Bool

Equations

Lean.isLetFun e = match Lean.letFunAnnotation? e with | none => false | some e => Lean.Expr.isApp e && Lean.Expr.isLambda (Lean.Expr.appFn! e)

source

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

Lean.Expr

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

Equations

Lean.mkInaccessible e = Lean.mkAnnotation `_inaccessible e

source

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

Option Lean.Expr

Equations

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

source

def Lean.patternWithRef? (p : Lean.Expr) :

Option (Lean.Syntax × Lean.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