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

Instances For