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

Equations

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

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.

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 __x ← Qq.getLevelQ' α match __x with | ⟨v, α⟩ => pure ⟨v, ⟨α, e⟩⟩

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?

Equations

• Qq.findLocalDeclWithTypeQ? sort = do let __x ← Lean.Meta.findLocalDeclWithType? q(«$sort») match __x with | some fvarId => pure (some (Lean.Expr.fvar fvarId)) | x => pure none

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

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

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

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

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

def Qq.mkIntNumeralQ {u : Lean.Level} (α : Q(Type u)) (i : Int) : Lean.MetaM Q(«$α»)

Build the numeral of the integer i in α: mkNumeral on the absolute value, negated if i is negative.

Equations

• Qq.mkIntNumeralQ α i = do let n ← Lean.Meta.mkNumeral α i.natAbs have n : Q(«$α») := n if i < 0 then do let __x ← Qq.synthInstanceQ q(Neg «$α») pure q(-«$n») else pure n

def Qq.mkRatNumeralQ {u : Lean.Level} (α : Q(Type u)) (r : Rat) : Lean.MetaM Q(«$α»)

Build the numeral of the rational r in α: the integer numeral of r.num if r is an integer, and otherwise p / q on the numerals of |r.num| and r.den, negated if r is negative, which is the form in which norm_num displays rationals.

Equations

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

def Qq.mkFinLitQ (n i : Nat) : Lean.MetaM Q(Fin «$n»)

Build the numeral i : Fin n.

Equations

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

def Qq.mkListLitQ {u : Lean.Level} {α : Q(Type u)} : List Q(«$α») → Q(List «$α»)

The list literal [a₀, …] of the entries as.

Equations

• Qq.mkListLitQ [] = q([])
• Qq.mkListLitQ (a :: as) = let mkListLitQ_1 := Qq.mkListLitQ as; q(«$a» :: «$mkListLitQ_1»)

def Qq.dropListLitQ {u : Lean.Level} {α : Q(Type u)} (n : Nat) (l : Q(List «$α»)) : Q(List «$α»)

List.drop n on the list literal l.

Equations

• One or more equations did not get rendered due to their size.
• Qq.dropListLitQ 0 l = l

def Qq.unconsListLitQ {u : Lean.Level} {α : Q(Type u)} (l : Q(List «$α»)) : Lean.MetaM ((hd : Q(«$α»)) × (tl : Q(List «$α»)) ×' «$l» =Q «$hd» :: «$tl»)

A specialised version of ~q($hd :: $tl).

Equations

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

def Qq.instantiateLevelMVarsQ (u : Lean.Level) : Lean.MetaM ((_u' : Lean.Level) ×' _u' =QL u)

Instantiate the level metavariables in u, remembering that the result is defeq to u.

This is a Qq version of Lean.instantiateLevelMVars.

Equations

• Qq.instantiateLevelMVarsQ u = do let __do_lift ← Lean.instantiateLevelMVars u pure ⟨__do_lift, ⋯⟩

def Qq.instantiateMVarsQ' {u : Lean.Level} {α : Q(Sort u)} (e : Q(«$α»)) : Lean.MetaM ((e' : Q(«$α»)) ×' «$e'» =Q «$e»)

Instantiate the metavariables in e, remembering that the result is defeq to e.

This is a variant of Qq.instantiateMVarsQ which returns the Qq-fact that the new expression is equal to the previous one.

Equations

• Qq.instantiateMVarsQ' e = do let __do_lift ← Qq.instantiateMVarsQ e pure ⟨__do_lift, ⋯⟩