Documentation

Qq.MetaM

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)