Documentation

Lean.Meta.AppBuilder

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

Equations

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.

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.

Return a proof of HEq a a.

Equations

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

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

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

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

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

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

Equations

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.

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 : HEq a b where a and b have the same type, returns a proof of Eq a b.

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

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).

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

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.

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.

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.

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

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.

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

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

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

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

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

Return a proof for p : Prop using decide p

Return a < b

Equations

Return @Classical.ofNonempty α _

Equations

Return sorryAx type

Equations

Return let_congr h₁ h₂

Equations

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

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

Equations
Equations
Equations

Return instance for [Monad m] if there is one

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.

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

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

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

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