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
- One or more equations did not get rendered due to their size.
Instances For
Return a local declaration whose type is definitionally equal to sort
.
This is a Qq version of Lean.Meta.findLocalDeclWithType?
Equations
- Qq.findLocalDeclWithTypeQ? sort = do let __discr ← Lean.Meta.findLocalDeclWithType? q(«$sort») match __discr with | some fvarId => pure (some (Lean.Expr.fvar fvarId)) | x => pure none
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 ℝ
.
Equations
- Qq.mkSetLiteralQ β [] x✝² x✝¹ x✝ = q(∅)
- Qq.mkSetLiteralQ β [x] x✝² x✝¹ x✝ = q({«$x»})
- Qq.mkSetLiteralQ β (x :: xs) x✝² x✝¹ x✝ = let mkSetLiteralQ_1 := Qq.mkSetLiteralQ β xs q(inferInstance) q(inferInstance) q(inferInstance); q(insert «$x» «$mkSetLiteralQ_1»)