Lean.Meta.AppBuilder

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.

source

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

Lean.MetaM Lean.Expr

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

Equations

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

source

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

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

source

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

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

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

source

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

Lean.MetaM Lean.Expr

Equations

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

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

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

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 (s : Lean.Expr) (fieldName : Lean.Name) :

Lean.MetaM Lean.Expr

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

source

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

Lean.MetaM Lean.Expr

Equations

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

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

Return Decidable.decide p

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

Return a proof for p : Prop using decide p

Equations

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

source

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

Lean.MetaM Lean.Expr

Return a < b

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

Return a <= b

Equations

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

source

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

Lean.MetaM Lean.Expr

Return Inhabited.default α

Equations

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

source

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

Lean.MetaM Lean.Expr

Return @Classical.ofNonempty α _

Equations

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

source

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

Lean.MetaM Lean.Expr

Return sorryAx type

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

Return funext h

Equations

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

source

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

Lean.MetaM Lean.Expr

Return propext h

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

Return let_congr h₁ h₂

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

Return let_val_congr b h

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

Return let_body_congr a h

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

Return of_eq_true h

Equations

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

source

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

Lean.MetaM Lean.Expr

Return eq_true h

Equations

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

source

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

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

source

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

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

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

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkImpDepCongrCtx h₁ h₂ = Lean.Meta.mkAppM `implies_dep_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)

Return instance for [Monad m] if there is one

Equations

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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