Documentation

Qq.AssertInstancesCommute

def Qq.Impl.findRedundantLocalInstQuoted? :
Lean.Elab.TermElabM (Option (Lean.FVarId × (u : Q(Lean.Level)) × (ty : Q(Q(Sort «$u»))) × Q(Q(«$$ty»)) × Q(Q(«$$ty»))))
Instances For