def
Qq.inferTypeQ
(e : Lean.Expr)
:
Lean.MetaM
((u : Lean.Level) ×
(α :
let u := u;
Q(Sort u)) ×
Q(«$α»))
Instances For
instance
Qq.instReprMaybeDefEq :
{u : Lean.Level} →
{α :
let u := u;
Q(Sort u)} →
{a b : Q(«$α»)} → Repr (Qq.MaybeDefEq a b)