# Documentation

Lean.Meta.AppBuilder

Return id e

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

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

Equations

Return a = b.

Equations

Return HEq a b.

Equations

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.

Return a proof of a = a.

Equations

Return a proof of HEq a a.

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

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

Equations

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

Equations

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₁ : Lean.Expr) (h₂ : Lean.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.

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₁ : Lean.Expr) (h₂ : Lean.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.

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.

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

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

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₁ : Lean.Expr) (h₂ : Lean.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 : Lean.Name) (xs : ) :

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 : Lean.Expr) (xs : ) :

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

Equations
def Lean.Meta.mkAppOptM (constName : Lean.Name) (xs : ) :

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 : Lean.Expr) (xs : ) :

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

Equations
def Lean.Meta.mkEqNDRec (motive : Lean.Expr) (h1 : Lean.Expr) (h2 : Lean.Expr) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.mkEqRec (motive : Lean.Expr) (h1 : Lean.Expr) (h2 : Lean.Expr) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.mkEqMP (eqProof : Lean.Expr) (pr : Lean.Expr) :
Equations
def Lean.Meta.mkEqMPR (eqProof : Lean.Expr) (pr : Lean.Expr) :
Equations
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.mkPure (monad : Lean.Expr) (e : Lean.Expr) :

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

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

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

def Lean.Meta.mkListLit (type : Lean.Expr) (xs : ) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.mkArrayLit (type : Lean.Expr) (xs : ) :
Equations
def Lean.Meta.mkSorry (type : Lean.Expr) (synthetic : Bool) :
Equations

Return Decidable.decide p

Equations

Return a proof for p : Prop using decide p

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

Return a < b

Equations

Return a <= b

Equations

Return Inhabited.default α

Equations

Return @Classical.ofNonempty α _

Equations

Return sorryAx type

Equations

Return funext h

Equations

Return propext h

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

Return let_congr h₁ h₂

Equations

Return let_val_congr b h

Equations

Return let_body_congr a h

Equations

Return of_eq_true h

Equations

Return eq_true h

Equations

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

Equations

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

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

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 : Lean.Expr) (n : Nat) :

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.

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

Equations

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

Equations

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

Equations

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

Equations

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

Equations

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

Equations