Equations
Instances For
Given proof
s.t. inferType proof
is definitionally equal to expectedProp
, returns
term @id expectedProp proof
.
Equations
Instances For
Given e
s.t. inferType e
is definitionally equal to expectedType
, returns
term @id expectedType e
.
Equations
Instances For
Given h : a = b
, returns a proof of b = a
.
Equations
Instances For
Given h₁ : a = b
and h₂ : b = c
, returns a proof of a = c
.
Equations
Instances For
If e
is @Eq.refl α a
, returns a
.
Equations
Instances For
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
Instances For
Given h₁ : f = g
and h₂ : a = b
, returns a proof of f a = g b
.
Equations
Instances For
Returns 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
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.
Equations
Instances For
Given a monad
and e : α
, makes pure e
.
Equations
Instances For
mkProjection s fieldName
returns an expression for accessing field fieldName
of the structure s
.
Remark: fieldName
may be a subfield of s
.
Returns a proof for p : Prop
using decide p
Equations
Instances For
Returns @Classical.ofNonempty α _
Equations
Instances For
Returns @of_eq_false p h
Equations
Instances For
Returns a + b
using a heterogeneous +
. This method assumes a
and b
have the same type.
Equations
Instances For
Returns a - b
using a heterogeneous -
. This method assumes a
and b
have the same type.
Equations
Instances For
Returns a * b
using a heterogeneous *
. This method assumes a
and b
have the same type.
Equations
Instances For
Returns a ≤ b
. This method assumes a
and b
have the same type.
Equations
Instances For
Returns a < b
. This method assumes a
and b
have the same type.
Equations
Instances For
Given h : a = b
, returns a proof for a ↔ b
.