def
Qq.inferTypeQ
(e : Lean.Expr)
:
Lean.MetaM
((u : Lean.Level) ×
(α :
let u := u;
Q(Sort u)) ×
Q(«$α»))
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
Qq.instReprMaybeDefEq :
{u : Lean.Level} →
{α :
let u := u;
Q(Sort u)} →
{a b : Q(«$α»)} → Repr (Qq.MaybeDefEq a b)
Equations
- One or more equations did not get rendered due to their size.