Extra Qq
helpers #
This file contains some additional functions for using the quote4 library more conveniently.
def
Qq.inferTypeQ'
(e : Lean.Expr)
:
Lean.MetaM
((u : Lean.Level) ×
(α :
let u := u;
Q(Type u)) ×
Q(«$α»))
Variant of inferTypeQ
that yields a type in Type u
rather than Sort u
.
Throws an error if the type is a Prop
or if it's otherwise not possible to represent
the universe as Type u
(for example due to universe level metavariables).
Equations
Instances For
Return a local declaration whose type is definitionally equal to sort
.
This is a Qq version of Lean.Meta.findLocalDeclWithType?
Equations
Instances For
Returns a proof of p : Prop
using decide p
.
This is a Qq version of Lean.Meta.mkDecideProof
.
Equations
Instances For
Join a list of elements of type α
into a container β
.
Usually β
is q(Multiset α)
or q(Finset α)
or q(Set α)
.
As an example
mkSetLiteralQ q(Finset ℝ) (List.range 4 |>.map fun n : ℕ ↦ q($n•π))
produces the expression {0 • π, 1 • π, 2 • π, 3 • π} : Finset ℝ
.