Given e s.t. inferType e is definitionally equal to expectedType, return
term @id expectedType e.
Instances For
Return a = b.
Instances For
Return HEq a b.
Instances For
Return a proof of a = a.
Instances For
Return a proof of HEq a a.
Instances For
Given hp : P and nhp : Not P returns an instance of type e.
Instances For
Given h : False, return an instance of type e.
Instances For
Given h : a = b, returns a proof of b = a.
Instances For
Given h₁ : a = b and h₂ : b = c returns a proof of a = c.
Instances For
Given f : α → β and h : a = b, returns a proof of f a = f b.
Instances For
Given h : f = g and a : α, returns a proof of f a = g a.
Instances For
Given h₁ : f = g and h₂ : a = b, returns a proof of f a = g b.
Instances For
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
Instances For
Similar to mkAppM, but takes an Expr instead of a constant name.
Instances For
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.
Instances For
Similar to mkAppOptM, but takes an Expr instead of a constant name
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Given a monad and e : α, makes pure e.
Instances For
mkProjection s fieldName return an expression for accessing field fieldName of the structure s.
Remark: fieldName may be a subfield of s.
Instances For
Instances For
Instances For
Return Decidable.decide p
Instances For
Return a proof for p : Prop using decide p
Instances For
Return a < b
Instances For
Return a <= b
Instances For
Return Inhabited.default α
Instances For
Return @Classical.ofNonempty α _
Instances For
Return sorryAx type
Instances For
Return let_congr h₁ h₂
Instances For
Return let_val_congr b h
Instances For
Return let_body_congr a h
Instances For
Return of_eq_true h
Instances For
Return eq_false h
h must have type definitionally equal to ¬ p in the current
reducibility setting.
Instances For
Instances For
Instances For
Return instance for [Monad m] if there is one
Instances For
Return (n : type), a numeric literal of type type. The method fails if we don't have an instance OfNat type n
Instances For
Return a + b using a heterogeneous +. This method assumes a and b have the same type.
Instances For
Return a - b using a heterogeneous -. This method assumes a and b have the same type.
Instances For
Return a * b using a heterogeneous *. This method assumes a and b have the same type.
Instances For
Return a ≤ b. This method assumes a and b have the same type.
Instances For
Return a < b. This method assumes a and b have the same type.
Instances For
Given h : a = b, return a proof for a ↔ b.