Qq
-ified spellings of functions in Lean.Meta
#
This file provides variants of the function in the Lean.Meta
namespace,
which operate with Q(_)
instead of Expr
.
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
A Qq
-ified version of Lean.Meta.inferType
Instead of writing let α ← inferType e
, this allows writing let ⟨u, α, e⟩ ← inferTypeQ e
,
which results in a context of
e✝ : Expr
u : Level
α : Q(Type u)
e : Q($α)
Here, the new e
is defeq to the old one, but now has Qq
-ascribed type information.
This is frequently useful when using the ~q
matching from QQ/Match.lean
,
as it allows an Expr
to be turned into something that can be matched upon.
Equations
Instances For
If e
is a ty
, then view it as a term of Q($ty)
.
Equations
Instances For
The result of Qq.isDefEqQ
; MaybeDefEq a b
is an optional version of $a =Q $b
.
- defEq {u : Lean.Level} {α : let u := u; Q(Sort u)} {a b : Q(«$α»)} : «$a» =Q «$b» → MaybeDefEq a b
- notDefEq {u : Lean.Level} {α : let u := u; Q(Sort u)} {a b : Q(«$α»)} : MaybeDefEq a b
Instances For
Equations
A version of Lean.Meta.isDefEq
which returns a strongly-typed witness rather than a bool.
Equations
Instances For
Like Qq.isDefEqQ
, but throws an error if not defeq.
Equations
Instances For
The result of Qq.isLevelDefEqQ
; MaybeLevelDefEq u v
is an optional version of $u =QL $v
.
- defEq {u v : Lean.Level} : u =QL v → MaybeLevelDefEq u v
- notDefEq {u v : Lean.Level} : MaybeLevelDefEq u v
Instances For
A version of Lean.Meta.isLevelDefEq
which returns a strongly-typed witness rather than a bool.