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

Return id e

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)

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

Given e s.t. inferType e is definitionally equal to expectedType, return term @id expectedType e.

Equations

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

def Lean.Meta.mkLetFun (x v e : Expr) : MetaM Expr

mkLetFun x v e creates the encoding for the let_fun x := v; e expression. The expression x can either be a free variable or a metavariable, and the function suitably abstracts x in e. NB: x must not be a let-bound free variable.

Equations

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

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

Return a = b.

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)

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

Return HEq a b.

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)

def Lean.Meta.mkEqHEq (a b : Expr) : MetaM Expr

If a and b have definitionally equal types, return Eq a b, otherwise return HEq a b.

Equations

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

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

Return a proof of a = a.

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)

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

Return a proof of HEq a a.

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)

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

Given hp : P and nhp : Not P returns an instance of type e.

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)

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

Given h : False, return an instance of type e.

Equations

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

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

Given h : a = b, returns a proof of b = a.

Equations

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

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

Given h₁ : a = b and h₂ : b = c returns a proof of a = c.

Equations

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

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

Similar to mkEqTrans, but arguments can be none. none is treated as a reflexivity proof.

Equations

• Lean.Meta.mkEqTrans? none none = pure none
• Lean.Meta.mkEqTrans? none (some h) = pure (some h)
• Lean.Meta.mkEqTrans? (some h) none = pure (some h)
• Lean.Meta.mkEqTrans? (some h₁) (some h₂) = do let a ← Lean.Meta.mkEqTrans h₁ h₂ pure (some a)

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

Given h : HEq a b, returns a proof of HEq b a.

Equations

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

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

Given h₁ : HEq a b, h₂ : HEq b c, returns a proof of HEq a c.

Equations

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

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

Given h : HEq a b where a and b have the same type, returns a proof of Eq a b.

Equations

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

def Lean.Meta.mkHEqOfEq (h : Expr) : MetaM Expr

Given h : Eq a b, returns a proof of HEq a b.

Equations

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

def Lean.Meta.isRefl? (e : Expr) : Option Expr

If e is @Eq.refl α a, return a.

Equations

• Lean.Meta.isRefl? e = if e.isAppOfArity `Eq.refl 2 = true then some e.appArg! else none

def Lean.Meta.congrArg? (e : Expr) : MetaM (Option (Expr × Expr × Expr))

If e is @congrArg α β a b f h, return α, f and h. Also works if e can be turned into such an application (e.g. congrFun).

Equations

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

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

Given f : α → β and h : a = b, returns a proof of f a = f b.

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

Given h : f = g and a : α, returns a proof of f a = g a.

Equations

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

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

Given h₁ : f = g and h₂ : a = b, returns a proof of f a = g b.

Equations

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

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

Return the application constName xs. It tries to fill the implicit arguments before the last element in xs.

Remark: mkAppM `arbitrary #[α] returns @arbitrary.{u} α without synthesizing the implicit argument occurring after α. Given a x : ([Decidable p] → Bool) × Nat, mkAppM `Prod.fst #[x] returns @Prod.fst ([Decidable p] → Bool) Nat x.

Equations

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

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

Similar to mkAppM, but takes an Expr instead of a constant name.

Equations

• Lean.Meta.mkAppM' f xs = do let fType ← Lean.Meta.inferType f Lean.Meta.withAppBuilderTrace✝ f xs (Lean.Meta.withNewMCtxDepth (Lean.Meta.mkAppMArgs✝ f fType xs))

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

Similar to mkAppM, but it allows us to specify which arguments are provided explicitly using Option type. Example: Given Pure.pure {m : Type u → Type v} [Pure m] {α : Type u} (a : α) : m α,

mkAppOptM `Pure.pure #[m, none, none, a]

returns a Pure.pure application if the instance Pure m can be synthesized, and the universe match. Note that,

mkAppM `Pure.pure #[a]

fails because the only explicit argument (a : α) is not sufficient for inferring the remaining arguments, we would need the expected type.

Equations

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

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

Similar to mkAppOptM, but takes an Expr instead of a constant name.

Equations

• Lean.Meta.mkAppOptM' f xs = do let fType ← Lean.Meta.inferType f Lean.Meta.withAppBuilderTrace✝ f xs (Lean.Meta.withNewMCtxDepth (Lean.Meta.mkAppOptMAux✝ f xs 0 #[] 0 #[] fType))

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Given a monad and e : α, makes pure e.

Equations

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

partial def Lean.Meta.mkProjection (s : Expr) (fieldName : Name) : MetaM Expr

mkProjection s fieldName returns an expression for accessing field fieldName of the structure s. Remark: fieldName may be a subfield of s.

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

Equations

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

def Lean.Meta.mkArrayLit (type : Expr) (xs : List Expr) : MetaM 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)

def Lean.Meta.mkNone (type : Expr) : MetaM Expr

Equations

• Lean.Meta.mkNone type = do let u ← Lean.Meta.getDecLevel type pure (Lean.mkApp (Lean.mkConst `Option.none [u]) type)

def Lean.Meta.mkSome (type value : Expr) : MetaM Expr

Equations

• Lean.Meta.mkSome type value = do let u ← Lean.Meta.getDecLevel type pure (Lean.mkApp2 (Lean.mkConst `Option.some [u]) type value)

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

Return Decidable.decide p

Equations

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

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

Return a proof for p : Prop using decide p

Equations

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

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

Return a < b

Equations

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

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

Return a <= b

Equations

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

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

Return Inhabited.default α

Equations

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

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

Return @Classical.ofNonempty α _

Equations

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

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

Return funext h

Equations

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

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

Return propext h

Equations

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

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

Return let_congr h₁ h₂

Equations

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

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

Return let_val_congr b h

Equations

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

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

Return let_body_congr a h

Equations

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

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

Return of_eq_true h

Equations

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

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

Return eq_true h

Equations

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

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

Return eq_false h h must have type definitionally equal to ¬ p in the current reducibility setting.

Equations

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

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

Return eq_false' h h must have type definitionally equal to p → False in the current reducibility setting.

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.mkImpDepCongrCtx (h₁ h₂ : Expr) : MetaM Expr

Equations

• Lean.Meta.mkImpDepCongrCtx h₁ h₂ = Lean.Meta.mkAppM `implies_dep_congr_ctx #[h₁, h₂]

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

Equations

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

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

Return instance for [Monad m] if there is one

Equations

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

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

Return (n : type), a numeric literal of type type. The method fails if we don't have an instance OfNat type n

Equations

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

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

Return a + b using a heterogeneous +. This method assumes a and b have the same type.

Equations

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

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

Return a - b using a heterogeneous -. This method assumes a and b have the same type.

Equations

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

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

Return a * b using a heterogeneous *. This method assumes a and b have the same type.

Equations

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

def Lean.Meta.mkLE (a b : Expr) : MetaM Expr

Return a ≤ b. This method assumes a and b have the same type.

Equations

• Lean.Meta.mkLE a b = Lean.Meta.mkBinaryRel✝ `LE `LE.le a b

def Lean.Meta.mkLT (a b : Expr) : MetaM Expr

Return a < b. This method assumes a and b have the same type.

Equations

• Lean.Meta.mkLT a b = Lean.Meta.mkBinaryRel✝ `LT `LT.lt a b

def Lean.Meta.mkIffOfEq (h : Expr) : MetaM Expr

Given h : a = b, return a proof for a ↔ b.

Equations

• Lean.Meta.mkIffOfEq h = if h.isAppOfArity `propext 3 = true then pure h.appArg! else Lean.Meta.mkAppM `Iff.of_eq #[h]