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.