Lean.Meta.AppBuilder

source

def Lean.Meta.mkId (e : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkId e = do let type ← Lean.Meta.inferType e let u ← Lean.Meta.getLevel type pure (Lean.mkApp2 (Lean.mkConst `id [u]) type e)

source

def Lean.Meta.mkExpectedTypeHint (e : Lean.Expr) (expectedType : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkExpectedTypeHint e expectedType = do let u ← Lean.Meta.getLevel expectedType pure (Lean.mkApp2 (Lean.mkConst `id [u]) expectedType e)

source

def Lean.Meta.mkEq (a : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkEq a b = do let aType ← Lean.Meta.inferType a let u ← Lean.Meta.getLevel aType pure (Lean.mkApp3 (Lean.mkConst `Eq [u]) aType a b)

source

def Lean.Meta.mkHEq (a : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkHEq a b = do let aType ← Lean.Meta.inferType a let bType ← Lean.Meta.inferType b let u ← Lean.Meta.getLevel aType pure (Lean.mkApp4 (Lean.mkConst `HEq [u]) aType a bType b)

source

def Lean.Meta.mkEqRefl (a : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkEqRefl a = do let aType ← Lean.Meta.inferType a let u ← Lean.Meta.getLevel aType pure (Lean.mkApp2 (Lean.mkConst `Eq.refl [u]) aType a)

source

def Lean.Meta.mkHEqRefl (a : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkHEqRefl a = do let aType ← Lean.Meta.inferType a let u ← Lean.Meta.getLevel aType pure (Lean.mkApp2 (Lean.mkConst `HEq.refl [u]) aType a)

source

def Lean.Meta.mkAbsurd (e : Lean.Expr) (hp : Lean.Expr) (hnp : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkAbsurd e hp hnp = do let p ← Lean.Meta.inferType hp let u ← Lean.Meta.getLevel e pure (Lean.mkApp4 (Lean.mkConst `absurd [u]) p e hp hnp)

source

def Lean.Meta.mkFalseElim (e : Lean.Expr) (h : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkFalseElim e h = do let u ← Lean.Meta.getLevel e pure (Lean.mkApp2 (Lean.mkConst `False.elim [u]) e h)

source

def Lean.Meta.mkEqSymm (h : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkEqSymm h = if Lean.Expr.isAppOf h `Eq.refl = true then pure h else do let hType ← Lean.Meta.infer h match Lean.Expr.eq? hType with | some (α, a, b) => do let u ← Lean.Meta.getLevel α pure (Lean.mkApp4 (Lean.mkConst `Eq.symm [u]) α a b h) | none => Lean.Meta.throwAppBuilderException `Eq.symm (Function.comp Lean.MessageData.ofFormat Lean.format "equality proof expected" ++ Lean.Meta.hasTypeMsg h hType)

source

def Lean.Meta.mkEqTrans (h₁ : Lean.Expr) (h₂ : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkEqTrans h₁ h₂ = if Lean.Expr.isAppOf h₁ `Eq.refl = true then pure h₂ else if Lean.Expr.isAppOf h₂ `Eq.refl = true then pure h₁ else do let hType₁ ← Lean.Meta.infer h₁ let hType₂ ← Lean.Meta.infer h₂ let _discr : Option (Lean.Expr × Lean.Expr × Lean.Expr) := Lean.Expr.eq? hType₂ match Lean.Expr.eq? hType₁, Lean.Expr.eq? hType₂ with | some (α, a, b), some (x, x_1, c) => do let u ← Lean.Meta.getLevel α pure (Lean.mkApp6 (Lean.mkConst `Eq.trans [u]) α a b c h₁ h₂) | none, x => Lean.Meta.throwAppBuilderException `Eq.trans (Function.comp Lean.MessageData.ofFormat Lean.format "equality proof expected" ++ Lean.Meta.hasTypeMsg h₁ hType₁) | x, none => Lean.Meta.throwAppBuilderException `Eq.trans (Function.comp Lean.MessageData.ofFormat Lean.format "equality proof expected" ++ Lean.Meta.hasTypeMsg h₂ hType₂)

source

def Lean.Meta.mkHEqSymm (h : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkHEqSymm h = if Lean.Expr.isAppOf h `HEq.refl = true then pure h else do let hType ← Lean.Meta.infer h match Lean.Expr.heq? hType with | some (α, a, β, b) => do let u ← Lean.Meta.getLevel α pure (Lean.mkApp5 (Lean.mkConst `HEq.symm [u]) α β a b h) | none => Lean.Meta.throwAppBuilderException `HEq.symm (Function.comp Lean.MessageData.ofFormat Lean.format "heterogeneous equality proof expected" ++ Lean.Meta.hasTypeMsg h hType)

source

def Lean.Meta.mkHEqTrans (h₁ : Lean.Expr) (h₂ : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkHEqTrans h₁ h₂ = if Lean.Expr.isAppOf h₁ `HEq.refl = true then pure h₂ else if Lean.Expr.isAppOf h₂ `HEq.refl = true then pure h₁ else do let hType₁ ← Lean.Meta.infer h₁ let hType₂ ← Lean.Meta.infer h₂ let _discr : Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr) := Lean.Expr.heq? hType₂ match Lean.Expr.heq? hType₁, Lean.Expr.heq? hType₂ with | some (α, a, β, b), some (x, x_1, γ, c) => do let u ← Lean.Meta.getLevel α pure (Lean.mkApp8 (Lean.mkConst `HEq.trans [u]) α β γ a b c h₁ h₂) | none, x => Lean.Meta.throwAppBuilderException `HEq.trans (Function.comp Lean.MessageData.ofFormat Lean.format "heterogeneous equality proof expected" ++ Lean.Meta.hasTypeMsg h₁ hType₁) | x, none => Lean.Meta.throwAppBuilderException `HEq.trans (Function.comp Lean.MessageData.ofFormat Lean.format "heterogeneous equality proof expected" ++ Lean.Meta.hasTypeMsg h₂ hType₂)

source

def Lean.Meta.mkEqOfHEq (h : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkEqOfHEq h = do let hType ← Lean.Meta.infer h match Lean.Expr.heq? hType with | some (α, a, β, b) => do let a_1 ← Lean.Meta.isDefEq α β let _do_jp : PUnit → Lean.MetaM Lean.Expr := fun y => do let u ← Lean.Meta.getLevel α pure (Lean.mkApp4 (Lean.mkConst `eq_of_heq [u]) α a b h) if a_1 = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.Meta.throwAppBuilderException `eq_of_heq (Lean.toMessageData "heterogeneous equality types are not definitionally equal" ++ Lean.toMessageData (Lean.indentExpr α) ++ Lean.toMessageData "\nis not definitionally equal to" ++ Lean.toMessageData (Lean.indentExpr β) ++ Lean.toMessageData "") _do_jp y | x => Lean.Meta.throwAppBuilderException `HEq.trans (Lean.toMessageData "heterogeneous equality proof expected" ++ Lean.toMessageData (Lean.indentExpr h) ++ Lean.toMessageData "")

source

def Lean.Meta.mkCongrArg (f : Lean.Expr) (h : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkCongrArg f h = if Lean.Expr.isAppOf h `Eq.refl = true then Lean.Meta.mkEqRefl (Lean.mkApp f (Lean.Expr.appArg! h)) else do let hType ← Lean.Meta.infer h let fType ← Lean.Meta.infer f let _discr : Option (Lean.Expr × Lean.Expr × Lean.Expr) := Lean.Expr.eq? hType match Lean.Expr.arrow? fType, Lean.Expr.eq? hType with | some (α, β), some (x, a, b) => do let u ← Lean.Meta.getLevel α let v ← Lean.Meta.getLevel β pure (Lean.mkApp6 (Lean.mkConst `congrArg [u, v]) α β a b f h) | none, x => Lean.Meta.throwAppBuilderException `congrArg (Function.comp Lean.MessageData.ofFormat Lean.format "non-dependent function expected" ++ Lean.Meta.hasTypeMsg f fType) | x, none => Lean.Meta.throwAppBuilderException `congrArg (Function.comp Lean.MessageData.ofFormat Lean.format "equality proof expected" ++ Lean.Meta.hasTypeMsg h hType)

source

def Lean.Meta.mkCongrFun (h : Lean.Expr) (a : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkCongrFun h a = if Lean.Expr.isAppOf h `Eq.refl = true then Lean.Meta.mkEqRefl (Lean.mkApp (Lean.Expr.appArg! h) a) else do let hType ← Lean.Meta.infer h match Lean.Expr.eq? hType with | some (ρ, f, g) => do let ρ ← Lean.Meta.whnfD ρ match ρ with | Lean.Expr.forallE n α β x => let β' := Lean.mkLambda n Lean.BinderInfo.default α β; do let u ← Lean.Meta.getLevel α let v ← Lean.Meta.getLevel (Lean.mkApp β' a) pure (Lean.mkApp6 (Lean.mkConst `congrFun [u, v]) α β' f g h a) | x => Lean.Meta.throwAppBuilderException `congrFun (Function.comp Lean.MessageData.ofFormat Lean.format "equality proof between functions expected" ++ Lean.Meta.hasTypeMsg h hType) | x => Lean.Meta.throwAppBuilderException `congrFun (Function.comp Lean.MessageData.ofFormat Lean.format "equality proof expected" ++ Lean.Meta.hasTypeMsg h hType)

source

def Lean.Meta.mkCongr (h₁ : Lean.Expr) (h₂ : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkCongr h₁ h₂ = if Lean.Expr.isAppOf h₁ `Eq.refl = true then Lean.Meta.mkCongrArg (Lean.Expr.appArg! h₁) h₂ else if Lean.Expr.isAppOf h₂ `Eq.refl = true then Lean.Meta.mkCongrFun h₁ (Lean.Expr.appArg! h₂) else do let hType₁ ← Lean.Meta.infer h₁ let hType₂ ← Lean.Meta.infer h₂ let _discr : Option (Lean.Expr × Lean.Expr × Lean.Expr) := Lean.Expr.eq? hType₂ match Lean.Expr.eq? hType₁, Lean.Expr.eq? hType₂ with | some (ρ, f, g), some (α, a, b) => do let ρ ← Lean.Meta.whnfD ρ match Lean.Expr.arrow? ρ with | some (x, β) => do let u ← Lean.Meta.getLevel α let v ← Lean.Meta.getLevel β pure (Lean.mkApp8 (Lean.mkConst `congr [u, v]) α β f g a b h₁ h₂) | x => Lean.Meta.throwAppBuilderException `congr (Function.comp Lean.MessageData.ofFormat Lean.format "non-dependent function expected" ++ Lean.Meta.hasTypeMsg h₁ hType₁) | none, x => Lean.Meta.throwAppBuilderException `congr (Function.comp Lean.MessageData.ofFormat Lean.format "equality proof expected" ++ Lean.Meta.hasTypeMsg h₁ hType₁) | x, none => Lean.Meta.throwAppBuilderException `congr (Function.comp Lean.MessageData.ofFormat Lean.format "equality proof expected" ++ Lean.Meta.hasTypeMsg h₂ hType₂)

source

def Lean.Meta.mkAppM (constName : Lean.Name) (xs : Array Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkAppM constName xs = Lean.traceCtx `Meta.appBuilder (Lean.Meta.withNewMCtxDepth do let discr ← Lean.Meta.mkFun constName let x : Lean.Expr × Lean.Expr := discr match x with | (f, fType) => do let r ← Lean.Meta.mkAppMArgs f fType xs let cls : Lean.Name := `Meta.appBuilder let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Lean.Expr := fun y => pure r if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "constName: " ++ Lean.toMessageData constName ++ Lean.toMessageData ", xs: " ++ Lean.toMessageData xs ++ Lean.toMessageData ", result: " ++ Lean.toMessageData r ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y)

source

def Lean.Meta.mkAppM' (f : Lean.Expr) (xs : Array Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkAppM' f xs = do let fType ← Lean.Meta.inferType f Lean.traceCtx `Meta.appBuilder (Lean.Meta.withNewMCtxDepth do let r ← Lean.Meta.mkAppMArgs f fType xs let cls : Lean.Name := `Meta.appBuilder let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Lean.Expr := fun y => pure r if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "f: " ++ Lean.toMessageData f ++ Lean.toMessageData ", xs: " ++ Lean.toMessageData xs ++ Lean.toMessageData ", result: " ++ Lean.toMessageData r ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y)

source

def Lean.Meta.mkAppOptM (constName : Lean.Name) (xs : Array (Option Lean.Expr)) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkAppOptM constName xs = Lean.traceCtx `Meta.appBuilder (Lean.Meta.withNewMCtxDepth do let discr ← Lean.Meta.mkFun constName let x : Lean.Expr × Lean.Expr := discr match x with | (f, fType) => Lean.Meta.mkAppOptMAux f xs 0 #[] 0 #[] fType)

source

def Lean.Meta.mkAppOptM' (f : Lean.Expr) (xs : Array (Option Lean.Expr)) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkAppOptM' f xs = do let fType ← Lean.Meta.inferType f Lean.traceCtx `Meta.appBuilder (Lean.Meta.withNewMCtxDepth (Lean.Meta.mkAppOptMAux f xs 0 #[] 0 #[] fType))

source

def Lean.Meta.mkEqNDRec (motive : Lean.Expr) (h1 : Lean.Expr) (h2 : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkEqNDRec motive h1 h2 = if Lean.Expr.isAppOf h2 `Eq.refl = true then pure h1 else do let h2Type ← Lean.Meta.infer h2 match Lean.Expr.eq? h2Type with | none => Lean.Meta.throwAppBuilderException `Eq.ndrec (Function.comp Lean.MessageData.ofFormat Lean.format "equality proof expected" ++ Lean.Meta.hasTypeMsg h2 h2Type) | some (α, a, b) => do let u2 ← Lean.Meta.getLevel α let motiveType ← Lean.Meta.infer motive match motiveType with | Lean.Expr.forallE x x_1 (Lean.Expr.sort u1 x_2) x_3 => pure (Lean.mkAppN (Lean.mkConst `Eq.ndrec [u1, u2]) #[α, a, motive, h1, b, h2]) | x => Lean.Meta.throwAppBuilderException `Eq.ndrec (Function.comp Lean.MessageData.ofFormat Lean.format "invalid motive" ++ Lean.indentExpr motive)

source

def Lean.Meta.mkEqRec (motive : Lean.Expr) (h1 : Lean.Expr) (h2 : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkEqRec motive h1 h2 = if Lean.Expr.isAppOf h2 `Eq.refl = true then pure h1 else do let h2Type ← Lean.Meta.infer h2 match Lean.Expr.eq? h2Type with | none => Lean.Meta.throwAppBuilderException `Eq.rec (Function.comp Lean.MessageData.ofFormat Lean.format "equality proof expected" ++ Lean.indentExpr h2) | some (α, a, b) => do let u2 ← Lean.Meta.getLevel α let motiveType ← Lean.Meta.infer motive match motiveType with | Lean.Expr.forallE x x_1 (Lean.Expr.forallE x_2 x_3 (Lean.Expr.sort u1 x_4) x_5) x_6 => pure (Lean.mkAppN (Lean.mkConst `Eq.rec [u1, u2]) #[α, a, motive, h1, b, h2]) | x => Lean.Meta.throwAppBuilderException `Eq.rec (Function.comp Lean.MessageData.ofFormat Lean.format "invalid motive" ++ Lean.indentExpr motive)

source

def Lean.Meta.mkEqMP (eqProof : Lean.Expr) (pr : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkEqMP eqProof pr = Lean.Meta.mkAppM `Eq.mp #[eqProof, pr]

source

def Lean.Meta.mkEqMPR (eqProof : Lean.Expr) (pr : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkEqMPR eqProof pr = Lean.Meta.mkAppM `Eq.mpr #[eqProof, pr]

source

def Lean.Meta.mkNoConfusion (target : Lean.Expr) (h : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkNoConfusion target h = do let type ← Lean.Meta.inferType h let type ← Lean.Meta.whnf type match Lean.Expr.eq? type with | none => Lean.Meta.throwAppBuilderException `noConfusion (Function.comp Lean.MessageData.ofFormat Lean.format "equality expected" ++ Lean.Meta.hasTypeMsg h type) | some (α, a, b) => do let α ← Lean.Meta.whnf α Lean.matchConstInduct (Lean.Expr.getAppFn α) (fun x => Lean.Meta.throwAppBuilderException `noConfusion (Function.comp Lean.MessageData.ofFormat Lean.format "inductive type expected" ++ Lean.indentExpr α)) fun v us => do let u ← Lean.Meta.getLevel target pure (Lean.mkAppN (Lean.mkConst (Lean.Name.mkStr v.toConstantVal.name "noConfusion") (u :: us)) (Lean.Expr.getAppArgs α ++ #[target, a, b, h]))

source

def Lean.Meta.mkPure (monad : Lean.Expr) (e : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkPure monad e = Lean.Meta.mkAppOptM `Pure.pure #[some monad, none, none, some e]

source

partial def Lean.Meta.mkProjection :

Lean.Expr → Lean.Name → Lean.MetaM Lean.Expr

source

def Lean.Meta.mkListLit (type : Lean.Expr) (xs : List Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkListLit type xs = do let u ← Lean.Meta.getDecLevel type let nil : Lean.Expr := Lean.mkApp (Lean.mkConst `List.nil [u]) type match xs with | [] => pure nil | x => let cons := Lean.mkApp (Lean.mkConst `List.cons [u]) type; pure (Lean.Meta.mkListLitAux nil cons xs)

source

def Lean.Meta.mkArrayLit (type : Lean.Expr) (xs : List Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkArrayLit type xs = do let u ← Lean.Meta.getDecLevel type let listLit ← Lean.Meta.mkListLit type xs pure (Lean.mkApp (Lean.mkApp (Lean.mkConst `List.toArray [u]) type) listLit)

source

def Lean.Meta.mkSorry (type : Lean.Expr) (synthetic : Bool) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkSorry type synthetic = do let u ← Lean.Meta.getLevel type pure (Lean.mkApp2 (Lean.mkConst `sorryAx [u]) type (Lean.toExpr synthetic))

source

def Lean.Meta.mkDecide (p : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkDecide p = Lean.Meta.mkAppOptM `Decidable.decide #[some p, none]

source

def Lean.Meta.mkDecideProof (p : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkDecideProof p = do let decP ← Lean.Meta.mkDecide p let decEqTrue ← Lean.Meta.mkEq decP (Lean.mkConst `Bool.true) let h ← Lean.Meta.mkEqRefl (Lean.mkConst `Bool.true) let h ← Lean.Meta.mkExpectedTypeHint h decEqTrue Lean.Meta.mkAppM `of_decide_eq_true #[h]

source

def Lean.Meta.mkLt (a : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkLt a b = Lean.Meta.mkAppM `LT.lt #[a, b]

source

def Lean.Meta.mkLe (a : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkLe a b = Lean.Meta.mkAppM `LE.le #[a, b]

source

def Lean.Meta.mkDefault (α : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkDefault α = Lean.Meta.mkAppOptM `Inhabited.default #[some α, none]

source

def Lean.Meta.mkOfNonempty (α : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkOfNonempty α = Lean.Meta.mkAppOptM `Classical.ofNonempty #[some α, none]

source

def Lean.Meta.mkSyntheticSorry (type : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkSyntheticSorry type = do let a ← Lean.Meta.getLevel type pure (Lean.mkApp2 (Lean.mkConst `sorryAx [a]) type (Lean.mkConst `Bool.true))

source

def Lean.Meta.mkFunExt (h : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkFunExt h = Lean.Meta.mkAppM `funext #[h]

source

def Lean.Meta.mkPropExt (h : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkPropExt h = Lean.Meta.mkAppM `propext #[h]

source

def Lean.Meta.mkLetCongr (h₁ : Lean.Expr) (h₂ : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkLetCongr h₁ h₂ = Lean.Meta.mkAppM `let_congr #[h₁, h₂]

source

def Lean.Meta.mkLetValCongr (b : Lean.Expr) (h : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkLetValCongr b h = Lean.Meta.mkAppM `let_val_congr #[b, h]

source

def Lean.Meta.mkLetBodyCongr (a : Lean.Expr) (h : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkLetBodyCongr a h = Lean.Meta.mkAppM `let_body_congr #[a, h]

source

def Lean.Meta.mkOfEqTrue (h : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkOfEqTrue h = Lean.Meta.mkAppM `of_eq_true #[h]

source

def Lean.Meta.mkEqTrue (h : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkEqTrue h = Lean.Meta.mkAppM `eq_true #[h]

source

def Lean.Meta.mkEqFalse (h : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkEqFalse h = Lean.Meta.mkAppM `eq_false #[h]

source

def Lean.Meta.mkEqFalse' (h : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkEqFalse' h = Lean.Meta.mkAppM `eq_false' #[h]

source

def Lean.Meta.mkImpCongr (h₁ : Lean.Expr) (h₂ : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkImpCongr h₁ h₂ = Lean.Meta.mkAppM `implies_congr #[h₁, h₂]

source

def Lean.Meta.mkImpCongrCtx (h₁ : Lean.Expr) (h₂ : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkImpCongrCtx h₁ h₂ = Lean.Meta.mkAppM `implies_congr_ctx #[h₁, h₂]

source

def Lean.Meta.mkForallCongr (h : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkForallCongr h = Lean.Meta.mkAppM `forall_congr #[h]

source

def Lean.Meta.isMonad? (m : Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

Equations

Lean.Meta.isMonad? m = tryCatch (do let monadType ← Lean.Meta.mkAppM `Monad #[m] let result ← Lean.Meta.trySynthInstance monadType none match result with | Lean.LOption.some inst => pure (some inst) | x => pure none) fun x => pure none

source

def Lean.Meta.mkNumeral (type : Lean.Expr) (n : Nat) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkNumeral type n = do let u ← Lean.Meta.getDecLevel type let inst ← Lean.Meta.synthInstance (Lean.mkApp2 (Lean.mkConst `OfNat [u]) type (Lean.mkRawNatLit n)) none pure (Lean.mkApp3 (Lean.mkConst `OfNat.ofNat [u]) type (Lean.mkRawNatLit n) inst)

source

def Lean.Meta.mkAdd (a : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkAdd a b = Lean.Meta.mkBinaryOp `HAdd `HAdd.hAdd a b

source

def Lean.Meta.mkSub (a : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkSub a b = Lean.Meta.mkBinaryOp `HSub `HSub.hSub a b

source

def Lean.Meta.mkMul (a : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkMul a b = Lean.Meta.mkBinaryOp `HMul `HMul.hMul a b