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

  • One or more equations did not get rendered due to their size.
Instances For
    theorem Qq.QuotedDefEq.rfl {u : Lean.Level} {α : Q(Sort u)} {a : Q(«$α»)} :
    «$a» =Q «$a»