Lean.Expr

Lean.BinderInfo.isExplicit x = match x with | Lean.BinderInfo.implicit => false | Lean.BinderInfo.strictImplicit => false | Lean.BinderInfo.instImplicit => false | x => true

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 x = match x with | Lean.BinderInfo.instImplicit => true | x => false

source

def Lean.BinderInfo.isImplicit :

Lean.BinderInfo → Bool

Equations

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

source

def Lean.BinderInfo.isStrictImplicit :

Lean.BinderInfo → Bool

Equations

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

source

def Lean.BinderInfo.isAuxDecl :

Lean.BinderInfo → Bool

Equations

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

source

@[inline]

abbrev Lean.MData :

Type

Equations

Lean.MData = Lean.KVMap

source

@[inline]

abbrev Lean.MData.empty :

Lean.MData

Equations

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

source

noncomputable def Lean.Expr.Data :

Type

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

Lean.Expr.Data.binderInfo c = let bi := UInt64.shiftRight (UInt64.shiftLeft c 24) 61; if (bi == 0) = true then Lean.BinderInfo.default else if (bi == 1) = true then Lean.BinderInfo.implicit else if (bi == 2) = true then Lean.BinderInfo.strictImplicit else if (bi == 3) = true then Lean.BinderInfo.instImplicit else Lean.BinderInfo.auxDecl

source

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

def Lean.BinderInfo.toUInt64 :

Lean.BinderInfo → UInt64

Equations

Lean.BinderInfo.toUInt64 x = match x with | Lean.BinderInfo.default => 0 | Lean.BinderInfo.implicit => 1 | Lean.BinderInfo.strictImplicit => 2 | Lean.BinderInfo.instImplicit => 3 | Lean.BinderInfo.auxDecl => 4

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

Lean.Expr.mkData h looseBVarRange approxDepth hasFVar hasExprMVar hasLevelMVar hasLevelParam bi nonDepLet = let approxDepth := if approxDepth > 255 then 255 else UInt32.toUInt8 approxDepth; if looseBVarRange > Nat.pow 2 16 - 1 then panicWithPosWithDecl "Lean.Expr" "Lean.Expr.mkData" 136 44 "bound variable index is too big" else let r := UInt32.toUInt64 (UInt64.toUInt32 h) + UInt64.shiftLeft (Bool.toUInt64 hasFVar) 32 + UInt64.shiftLeft (Bool.toUInt64 hasExprMVar) 33 + UInt64.shiftLeft (Bool.toUInt64 hasLevelMVar) 34 + UInt64.shiftLeft (Bool.toUInt64 hasLevelParam) 35 + UInt64.shiftLeft (Bool.toUInt64 nonDepLet) 36 + UInt64.shiftLeft (Lean.BinderInfo.toUInt64 bi) 37 + UInt64.shiftLeft (UInt8.toUInt64 approxDepth) 40 + UInt64.shiftLeft (Nat.toUInt64 looseBVarRange) 48; r

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

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

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

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

source

instance Lean.instReprData_1 :

Repr Lean.Expr.Data

Equations

Lean.instReprData_1 = { reprPrec := fun v prec => Id.run (let r := "Expr.mkData " ++ toString (Lean.Expr.Data.hash v); let _do_jp := fun r y => let _do_jp := fun r y => let _do_jp := fun r y => let _do_jp := fun r y => let _do_jp := fun r y => let _do_jp := fun r y => let _do_jp := fun r y => Repr.addAppParen (Std.Format.text r) prec; if (Lean.Expr.Data.binderInfo v == Lean.BinderInfo.default) = true then let r := r ++ " (bi := " ++ toString (repr (Lean.Expr.Data.binderInfo v)) ++ ")"; do let y ← pure PUnit.unit _do_jp r y else do let y ← pure PUnit.unit _do_jp r y; if Lean.Expr.Data.nonDepLet v = true then let r := r ++ " (nonDepLet := " ++ toString (Lean.Expr.Data.nonDepLet v) ++ ")"; do let y ← pure PUnit.unit _do_jp r y else do let y ← pure PUnit.unit _do_jp r y; if Lean.Expr.Data.hasLevelMVar v = true then let r := r ++ " (hasLevelMVar := " ++ toString (Lean.Expr.Data.hasLevelMVar v) ++ ")"; do let y ← pure PUnit.unit _do_jp r y else do let y ← pure PUnit.unit _do_jp r y; if Lean.Expr.Data.hasExprMVar v = true then let r := r ++ " (hasExprMVar := " ++ toString (Lean.Expr.Data.hasExprMVar v) ++ ")"; do let y ← pure PUnit.unit _do_jp r y else do let y ← pure PUnit.unit _do_jp r y; if Lean.Expr.Data.hasFVar v = true then let r := r ++ " (hasFVar := " ++ toString (Lean.Expr.Data.hasFVar v) ++ ")"; do let y ← pure PUnit.unit _do_jp r y else do let y ← pure PUnit.unit _do_jp r y; if (Lean.Expr.Data.approxDepth v != 0) = true then let r := r ++ " (approxDepth := " ++ toString (Lean.Expr.Data.approxDepth v) ++ ")"; do let y ← pure PUnit.unit _do_jp r y else do let y ← pure PUnit.unit _do_jp r y; if (Lean.Expr.Data.looseBVarRange v != 0) = true then let r := r ++ " (looseBVarRange := " ++ toString (Lean.Expr.Data.looseBVarRange v) ++ ")"; do let y ← pure PUnit.unit _do_jp r y else do let y ← pure PUnit.unit _do_jp r y) }

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

noncomputable 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

noncomputable def Lean.FVarIdHashSet :

Type

Equations

Lean.FVarIdHashSet = Std.HashSet Lean.FVarId

source

noncomputable 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.instReprExpr :

Repr Lean.Expr

Equations

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

source

instance Lean.instInhabitedExpr :

Inhabited Lean.Expr

Equations

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

source

@[inline]

def Lean.Expr.data :

Lean.Expr → Lean.Expr.Data

Equations

Lean.Expr.data x = match x with | Lean.Expr.bvar x d => d | Lean.Expr.fvar x d => d | Lean.Expr.mvar x d => d | Lean.Expr.sort x d => d | Lean.Expr.const x x_1 d => d | Lean.Expr.app x x_1 d => d | Lean.Expr.lam x x_1 x_2 d => d | Lean.Expr.forallE x x_1 x_2 d => d | Lean.Expr.letE x x_1 x_2 x_3 d => d | Lean.Expr.lit x d => d | Lean.Expr.mdata x x_1 d => d | Lean.Expr.proj x x_1 x_2 d => d

source

def Lean.Expr.ctorName :

Lean.Expr → String

Equations

Lean.Expr.ctorName x = match x with | Lean.Expr.bvar x x_1 => "bvar" | Lean.Expr.fvar x x_1 => "fvar" | Lean.Expr.mvar x x_1 => "mvar" | Lean.Expr.sort x x_1 => "sort" | Lean.Expr.const x x_1 x_2 => "const" | Lean.Expr.app x x_1 x_2 => "app" | Lean.Expr.lam x x_1 x_2 x_3 => "lam" | Lean.Expr.forallE x x_1 x_2 x_3 => "forallE" | Lean.Expr.letE x x_1 x_2 x_3 x_4 => "letE" | Lean.Expr.lit x x_1 => "lit" | Lean.Expr.mdata x x_1 x_2 => "mdata" | Lean.Expr.proj x x_1 x_2 x_3 => "proj"

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

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

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

def Lean.Expr.hashEx :

Lean.Expr → UInt64

Equations

Lean.Expr.hashEx = hash

source

def Lean.Expr.hasFVarEx :

Lean.Expr → Bool

Equations

Lean.Expr.hasFVarEx = Lean.Expr.hasFVar

source

def Lean.Expr.hasExprMVarEx :

Lean.Expr → Bool

Equations

Lean.Expr.hasExprMVarEx = Lean.Expr.hasExprMVar

source

def Lean.Expr.hasLevelMVarEx :

Lean.Expr → Bool

Equations

Lean.Expr.hasLevelMVarEx = Lean.Expr.hasLevelMVar

source

def Lean.Expr.hasMVarEx :

Lean.Expr → Bool

Equations

Lean.Expr.hasMVarEx = Lean.Expr.hasMVar

source

def Lean.Expr.hasLevelParamEx :

Lean.Expr → Bool

Equations

Lean.Expr.hasLevelParamEx = Lean.Expr.hasLevelParam

source

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

UInt32

Equations

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

source

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

Lean.mkConst n lvls = Lean.Expr.const n lvls (Lean.Expr.mkData (mixHash 5 (mixHash (hash n) (hash lvls))) 0 0 false false (List.any lvls Lean.Level.hasMVar) (List.any lvls Lean.Level.hasParam) Lean.BinderInfo.default)

source

def Lean.Literal.type :

Lean.Literal → Lean.Expr

Equations

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

source

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

Lean.mkMData m e = let d := Lean.Expr.approxDepth e + 1; Lean.Expr.mdata m e (Lean.Expr.mkData (mixHash (UInt32.toUInt64 d) (hash e)) (Lean.Expr.looseBVarRange e) d (Lean.Expr.hasFVar e) (Lean.Expr.hasExprMVar e) (Lean.Expr.hasLevelMVar e) (Lean.Expr.hasLevelParam e) Lean.BinderInfo.default)

source

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

Lean.Expr

Equations

Lean.mkProj s i e = let d := Lean.Expr.approxDepth e + 1; Lean.Expr.proj s i e (Lean.Expr.mkData (mixHash (UInt32.toUInt64 d) (mixHash (hash s) (mixHash (hash i) (hash e)))) (Lean.Expr.looseBVarRange e) d (Lean.Expr.hasFVar e) (Lean.Expr.hasExprMVar e) (Lean.Expr.hasLevelMVar e) (Lean.Expr.hasLevelParam e) Lean.BinderInfo.default)

source

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

Lean.Expr

Equations

Lean.mkApp f a = let d := max (Lean.Expr.approxDepth f) (Lean.Expr.approxDepth a) + 1; Lean.Expr.app f a (Lean.Expr.mkData (mixHash (UInt32.toUInt64 d) (mixHash (hash f) (hash a))) (max (Lean.Expr.looseBVarRange f) (Lean.Expr.looseBVarRange a)) d (Lean.Expr.hasFVar f || Lean.Expr.hasFVar a) (Lean.Expr.hasExprMVar f || Lean.Expr.hasExprMVar a) (Lean.Expr.hasLevelMVar f || Lean.Expr.hasLevelMVar a) (Lean.Expr.hasLevelParam f || Lean.Expr.hasLevelParam a) Lean.BinderInfo.default)

source

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

Lean.Expr

Equations

Lean.mkLambda x bi t b = let d := max (Lean.Expr.approxDepth t) (Lean.Expr.approxDepth b) + 1; Lean.Expr.lam x t b (Lean.Expr.mkDataForBinder (mixHash (UInt32.toUInt64 d) (mixHash (hash t) (hash b))) (max (Lean.Expr.looseBVarRange t) (Lean.Expr.looseBVarRange b - 1)) d (Lean.Expr.hasFVar t || Lean.Expr.hasFVar b) (Lean.Expr.hasExprMVar t || Lean.Expr.hasExprMVar b) (Lean.Expr.hasLevelMVar t || Lean.Expr.hasLevelMVar b) (Lean.Expr.hasLevelParam t || Lean.Expr.hasLevelParam b) bi)

source

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

Lean.Expr

Equations

Lean.mkForall x bi t b = let d := max (Lean.Expr.approxDepth t) (Lean.Expr.approxDepth b) + 1; Lean.Expr.forallE x t b (Lean.Expr.mkDataForBinder (mixHash (UInt32.toUInt64 d) (mixHash (hash t) (hash b))) (max (Lean.Expr.looseBVarRange t) (Lean.Expr.looseBVarRange b - 1)) d (Lean.Expr.hasFVar t || Lean.Expr.hasFVar b) (Lean.Expr.hasExprMVar t || Lean.Expr.hasExprMVar b) (Lean.Expr.hasLevelMVar t || Lean.Expr.hasLevelMVar b) (Lean.Expr.hasLevelParam t || Lean.Expr.hasLevelParam b) bi)

source

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

Lean.Expr

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

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

Lean.mkLet x t v b nonDep = let d := max (max (Lean.Expr.approxDepth t) (Lean.Expr.approxDepth v)) (Lean.Expr.approxDepth b) + 1; Lean.Expr.letE x t v b (Lean.Expr.mkDataForLet (mixHash (UInt32.toUInt64 d) (mixHash (hash t) (mixHash (hash v) (hash b)))) (max (max (Lean.Expr.looseBVarRange t) (Lean.Expr.looseBVarRange v)) (Lean.Expr.looseBVarRange b - 1)) d (Lean.Expr.hasFVar t || Lean.Expr.hasFVar v || Lean.Expr.hasFVar b) (Lean.Expr.hasExprMVar t || Lean.Expr.hasExprMVar v || Lean.Expr.hasExprMVar b) (Lean.Expr.hasLevelMVar t || Lean.Expr.hasLevelMVar v || Lean.Expr.hasLevelMVar b) (Lean.Expr.hasLevelParam t || Lean.Expr.hasLevelParam v || Lean.Expr.hasLevelParam b) nonDep)

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

def Lean.mkBVarEx :

Nat → Lean.Expr

Equations

Lean.mkBVarEx = Lean.mkBVar

source

def Lean.mkFVarEx :

Lean.FVarId → Lean.Expr

Equations

Lean.mkFVarEx = Lean.mkFVar

source

def Lean.mkMVarEx :

Lean.MVarId → Lean.Expr

Equations

Lean.mkMVarEx = Lean.mkMVar

source

def Lean.mkSortEx :

Lean.Level → Lean.Expr

Equations

Lean.mkSortEx = Lean.mkSort

source

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

Lean.Expr

Equations

Lean.mkConstEx c lvls = Lean.mkConst c lvls

source

def Lean.mkAppEx :

Lean.Expr → Lean.Expr → Lean.Expr

Equations

Lean.mkAppEx = Lean.mkApp

source

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

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

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

def Lean.mkLitEx :

Lean.Literal → Lean.Expr

Equations

Lean.mkLitEx = Lean.mkLit

source

def Lean.mkMDataEx :

Lean.MData → Lean.Expr → Lean.Expr

Equations

Lean.mkMDataEx = Lean.mkMData

source

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

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

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

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]

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

String

source

@[extern lean_expr_quick_lt]

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

Bool

source

@[extern lean_expr_lt]

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

Bool

source

@[extern lean_expr_eqv]

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

Bool

source

instance Lean.Expr.instBEqExpr :

BEq Lean.Expr

Equations

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

source

@[extern lean_expr_equal]

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

Bool

source

def Lean.Expr.isSort :

Lean.Expr → Bool

Equations

Lean.Expr.isSort x = match x with | Lean.Expr.sort x x_1 => true | x => false

source

def Lean.Expr.isType :

Lean.Expr → Bool

Equations

Lean.Expr.isType x = match x with | Lean.Expr.sort (Lean.Level.succ x x_1) x_2 => true | x => false

source

def Lean.Expr.isProp :

Lean.Expr → Bool

Equations

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

source

def Lean.Expr.isBVar :

Lean.Expr → Bool

Equations

Lean.Expr.isBVar x = match x with | Lean.Expr.bvar x x_1 => true | x => false

source

def Lean.Expr.isMVar :

Lean.Expr → Bool

Equations

Lean.Expr.isMVar x = match x with | Lean.Expr.mvar x x_1 => true | x => false

source

def Lean.Expr.isFVar :

Lean.Expr → Bool

Equations

Lean.Expr.isFVar x = match x with | Lean.Expr.fvar x x_1 => true | x => false

source

def Lean.Expr.isApp :

Lean.Expr → Bool

Equations

Lean.Expr.isApp x = match x with | Lean.Expr.app x x_1 x_2 => true | x => false

source

def Lean.Expr.isProj :

Lean.Expr → Bool

Equations

Lean.Expr.isProj x = match x with | Lean.Expr.proj x x_1 x_2 x_3 => true | x => false

source

def Lean.Expr.isConst :

Lean.Expr → Bool

Equations

Lean.Expr.isConst x = match x with | Lean.Expr.const x x_1 x_2 => true | x => false

source

def Lean.Expr.isConstOf :

Lean.Expr → Lean.Name → Bool

Equations

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

source

def Lean.Expr.isForall :

Lean.Expr → Bool

Equations

Lean.Expr.isForall x = match x with | Lean.Expr.forallE x x_1 x_2 x_3 => true | x => false

source

def Lean.Expr.isLambda :

Lean.Expr → Bool

Equations

Lean.Expr.isLambda x = match x with | Lean.Expr.lam x x_1 x_2 x_3 => true | x => false

source

def Lean.Expr.isBinding :

Lean.Expr → Bool

Equations

Lean.Expr.isBinding x = match x with | Lean.Expr.lam x x_1 x_2 x_3 => true | Lean.Expr.forallE x x_1 x_2 x_3 => true | x => false

source

def Lean.Expr.isLet :

Lean.Expr → Bool

Equations

Lean.Expr.isLet x = match x with | Lean.Expr.letE x x_1 x_2 x_3 x_4 => true | x => false

source

def Lean.Expr.isMData :

Lean.Expr → Bool

Equations

Lean.Expr.isMData x = match x with | Lean.Expr.mdata x x_1 x_2 => true | x => false

source

def Lean.Expr.isLit :

Lean.Expr → Bool

Equations

Lean.Expr.isLit x = match x with | Lean.Expr.lit x x_1 => true | x => false

source

def Lean.Expr.getForallBody :

Lean.Expr → Lean.Expr

Equations

Lean.Expr.getForallBody (Lean.Expr.forallE x_1 x_2 x_3 x_4) = Lean.Expr.getForallBody x_3
Lean.Expr.getForallBody x = x

source

def Lean.Expr.getAppFn :

Lean.Expr → Lean.Expr

Equations

Lean.Expr.getAppFn (Lean.Expr.app x_1 x_2 x_3) = Lean.Expr.getAppFn x_1
Lean.Expr.getAppFn x = x

source

def Lean.Expr.getAppNumArgsAux :

Lean.Expr → Nat → Nat

Equations

Lean.Expr.getAppNumArgsAux (Lean.Expr.app f a x_2) x = Lean.Expr.getAppNumArgsAux f (x + 1)
Lean.Expr.getAppNumArgsAux x x = x

source

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

Nat

Equations

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

source

@[inline]

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

Array Lean.Expr

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

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 x_3) x x = Lean.Expr.withAppAux k f (Array.set! x x a) (x - 1)
Lean.Expr.withAppAux k x x x = k x x

source

@[inline]

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

α

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

@[inline]

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

α

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

source

def Lean.Expr.getRevArg! :

Lean.Expr → Nat → Lean.Expr

source

@[inline]

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

Lean.Expr

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

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

Equations

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

source

def Lean.Expr.isAppOfArity :

Lean.Expr → Lean.Name → Nat → Bool

source

def Lean.Expr.appFn! :

Lean.Expr → Lean.Expr

Equations

Lean.Expr.appFn! x = match x with | Lean.Expr.app f x x_1 => f | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appFn!" 586 17 "application expected"

source

def Lean.Expr.appArg! :

Lean.Expr → Lean.Expr

Equations

Lean.Expr.appArg! x = match x with | Lean.Expr.app x a x_1 => a | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.appArg!" 590 17 "application expected"

source

def Lean.Expr.sortLevel! :

Lean.Expr → Lean.Level

Equations

Lean.Expr.sortLevel! x = match x with | Lean.Expr.sort u x => u | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.sortLevel!" 594 17 "sort expected"

source

def Lean.Expr.litValue! :

Lean.Expr → Lean.Literal

Equations

Lean.Expr.litValue! x = match x with | Lean.Expr.lit v x => v | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.litValue!" 598 16 "literal expected"

source

def Lean.Expr.isNatLit :

Lean.Expr → Bool

Equations

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

source

def Lean.Expr.natLit? :

Lean.Expr → Option Nat

Equations

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

source

def Lean.Expr.isStringLit :

Lean.Expr → Bool

Equations

Lean.Expr.isStringLit x = match x with | Lean.Expr.lit (Lean.Literal.strVal x) x_1 => 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

Lean.Expr.constName! x = match x with | Lean.Expr.const n x x_1 => n | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.constName!" 617 19 "constant expected"

source

def Lean.Expr.constName? :

Lean.Expr → Option Lean.Name

Equations

Lean.Expr.constName? x = match x with | Lean.Expr.const n x x_1 => some n | x => none

source

def Lean.Expr.constLevels! :

Lean.Expr → List Lean.Level

Equations

Lean.Expr.constLevels! x = match x with | Lean.Expr.const x ls x_1 => ls | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.constLevels!" 625 20 "constant expected"

source

def Lean.Expr.bvarIdx! :

Lean.Expr → Nat

Equations

Lean.Expr.bvarIdx! x = match x with | Lean.Expr.bvar idx x => idx | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.bvarIdx!" 629 18 "bvar expected"

source

def Lean.Expr.fvarId! :

Lean.Expr → Lean.FVarId

Equations

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

source

def Lean.Expr.mvarId! :

Lean.Expr → Lean.MVarId

Equations

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

source

def Lean.Expr.bindingName! :

Lean.Expr → Lean.Name

Equations

Lean.Expr.bindingName! x = match x with | Lean.Expr.forallE n x x_1 x_2 => n | Lean.Expr.lam n x x_1 x_2 => n | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.bindingName!" 642 23 "binding expected"

source

def Lean.Expr.bindingDomain! :

Lean.Expr → Lean.Expr

Equations

Lean.Expr.bindingDomain! x = match x with | Lean.Expr.forallE x d x_1 x_2 => d | Lean.Expr.lam x d x_1 x_2 => d | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.bindingDomain!" 647 23 "binding expected"

source

def Lean.Expr.bindingBody! :

Lean.Expr → Lean.Expr

Equations

Lean.Expr.bindingBody! x = match x with | Lean.Expr.forallE x x_1 b x_2 => b | Lean.Expr.lam x x_1 b x_2 => b | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.bindingBody!" 652 23 "binding expected"

source

def Lean.Expr.bindingInfo! :

Lean.Expr → Lean.BinderInfo

Equations

Lean.Expr.bindingInfo! x = match x with | Lean.Expr.forallE x x_1 x_2 c => Lean.Expr.Data.binderInfo c | Lean.Expr.lam x x_1 x_2 c => Lean.Expr.Data.binderInfo c | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.bindingInfo!" 657 23 "binding expected"

source

def Lean.Expr.letName! :

Lean.Expr → Lean.Name

Equations

Lean.Expr.letName! x = match x with | Lean.Expr.letE n x x_1 x_2 x_3 => n | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.letName!" 661 17 "let expression expected"

source

def Lean.Expr.letType! :

Lean.Expr → Lean.Expr

Equations

Lean.Expr.letType! x = match x with | Lean.Expr.letE x t x_1 x_2 x_3 => t | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.letType!" 665 19 "let expression expected"

source

def Lean.Expr.letValue! :

Lean.Expr → Lean.Expr

Equations

Lean.Expr.letValue! x = match x with | Lean.Expr.letE x x_1 v x_2 x_3 => v | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.letValue!" 669 21 "let expression expected"

source

def Lean.Expr.letBody! :

Lean.Expr → Lean.Expr

Equations

Lean.Expr.letBody! x = match x with | Lean.Expr.letE x x_1 x_2 b x_3 => b | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.letBody!" 673 23 "let expression expected"

source

def Lean.Expr.consumeMData :

Lean.Expr → Lean.Expr

Equations

Lean.Expr.consumeMData (Lean.Expr.mdata x_1 x_2 x_3) = Lean.Expr.consumeMData x_2
Lean.Expr.consumeMData x = x

source

def Lean.Expr.mdataExpr! :

Lean.Expr → Lean.Expr

Equations

Lean.Expr.mdataExpr! x = match x with | Lean.Expr.mdata x e x_1 => e | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.mdataExpr!" 681 19 "mdata expression expected"

source

def Lean.Expr.projExpr! :

Lean.Expr → Lean.Expr

Equations

Lean.Expr.projExpr! x = match x with | Lean.Expr.proj x x_1 e x_2 => e | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.projExpr!" 685 20 "proj expression expected"

source

def Lean.Expr.projIdx! :

Lean.Expr → Nat

Equations

Lean.Expr.projIdx! x = match x with | Lean.Expr.proj x i x_1 x_2 => i | x => panicWithPosWithDecl "Lean.Expr" "Lean.Expr.projIdx!" 689 20 "proj expression expected"