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.

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 __discr ← Lean.Meta.findLocalDeclWithType? q(«$sort») match __discr 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