Extra Qq helpers

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

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

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

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

theorem Qq.QuotedDefEq.rfl {u : Lean.Level} {α : Q(Sort u)} {a : Q(«$α»)} : «$a» =Q «$a»

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?

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.

def Qq.mkSetLiteralQ {u v : Lean.Level} {α : Q(Type u)} (β : Q(Type v)) (elems : List Q(«$α»)) : autoParam Q(EmptyCollection «$β») mkSetLiteralQ._auto_1 → autoParam Q(Singleton «$α» «$β») mkSetLiteralQ._auto_3 → autoParam Q(Insert «$α» «$β») mkSetLiteralQ._auto_5 → 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 ℝ.

def Qq.mkNatLitQ (n : ℕ) : Q(ℕ)

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.

def Qq.mkIntLitQ (n : ℤ) : Q(ℤ)

Returns the integer literal n.

This is a Qq version of Lean.mkIntLit.