# Extra `Qq` helpers #

This file contains some additional functions for using the quote4 library more conveniently.

source
def Qq.getLevelQ (e : Lean.Expr) :
Lean.MetaM ((u : Lean.Level) × Q(Sort u))

If `e` has type `Sort u` for some level `u`, return `u` and `e : Q(Sort u)`.

Equations

- Qq.getLevelQ e = do let __do_lift ← Lean.Meta.getLevel e pure ⟨__do_lift, e⟩

Instances For

source
def Qq.getLevelQ' (e : Lean.Expr) :
Lean.MetaM ((u : Lean.Level) × Q(Type u))

If `e` has type `Type u` for some level `u`, return `u` and `e : Q(Type u)`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Qq.inferTypeQ' (e : Lean.Expr) :
Lean.MetaM ((u : Lean.Level) × (α : have 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

- Qq.inferTypeQ' e = do let α ← Lean.Meta.inferType e let __discr ← Qq.getLevelQ' α match __discr with | ⟨v, α⟩ => pure ⟨v, ⟨α, e⟩⟩

Instances For

source
theorem Qq.QuotedDefEq.rfl {u : Lean.Level} {α : Q(Sort u)} {a : Q(«$α»)} :
«$a» =Q «$a»
source
def Qq.findLocalDeclWithTypeQ? {u : Lean.Level} (sort : Q(Sort u)) :
Lean.MetaM (Option Q(«$sort»))

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

source
def Qq.mkDecideProofQ (p : Q(Prop)) :
Lean.MetaM Q(«$p»)

Returns a proof of `p : Prop` using `decide p`.

This is a Qq version of `Lean.Meta.mkDecideProof`.

Equations

- Qq.mkDecideProofQ p = Lean.Meta.mkDecideProof p

Instances For

source
def Qq.mkSetLiteralQ {u v : Lean.Level} {α : Q(Type u)} (β : Q(Type v)) (elems : List Q(«$α»)) :
autoParam Q(EmptyCollection «$β») _auto✝ → autoParam Q(Singleton «$α» «$β») _auto✝¹ → autoParam Q(Insert «$α» «$β») _auto✝² → Q(«$β»)

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»)

Instances For

source
def Qq.mkNatLitQ (n : Nat) :
Q(Nat)

Returns the natural number literal `n` as used in the frontend. It is a `OfNat.ofNat` application. Recall that all theorems and definitions containing numeric literals are encoded using `OfNat.ofNat` applications in the frontend.

This is a Qq version of `Lean.mkNatLit`.

Equations

- Qq.mkNatLitQ n = Lean.mkNatLit n

Instances For

source
def Qq.mkIntLitQ (n : Int) :
Q(Int)

Returns the integer literal `n`.

This is a Qq version of `Lean.mkIntLit`.

Equations

- Qq.mkIntLitQ n = Lean.mkIntLit n

Instances For