def Qq.termAssumeInstancesCommute'_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Qq.Impl.isRedundantLocalInst? (inst : Lean.FVarId) : Lean.MetaM (Option Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.

def Qq.Impl.findRedundantLocalInst? : Qq.Impl.QuoteM (Option (Lean.FVarId × Lean.Expr))

Equations

• One or more equations did not get rendered due to their size.

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»))))

Equations

• One or more equations did not get rendered due to their size.

def Qq.Impl.termAssertInstancesCommuteImpl_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Qq.Impl.termAssertInstancesCommuteDummy : Lean.ParserDescr

Equations

• Qq.Impl.termAssertInstancesCommuteDummy = Lean.ParserDescr.node `Qq.Impl.termAssertInstancesCommuteDummy 1024 (Lean.ParserDescr.symbol "assertInstancesCommuteDummy")

def Qq.Impl.termAssumeInstancesCommuteDummy : Lean.ParserDescr

Equations

• Qq.Impl.termAssumeInstancesCommuteDummy = Lean.ParserDescr.node `Qq.Impl.termAssumeInstancesCommuteDummy 1024 (Lean.ParserDescr.symbol "assumeInstancesCommuteDummy")

def Qq.doElemAssertInstancesCommute : Lean.ParserDescr

Equations

• Qq.doElemAssertInstancesCommute = Lean.ParserDescr.node `Qq.doElemAssertInstancesCommute 1024 (Lean.ParserDescr.symbol "assertInstancesCommute")

def Qq.doElemAssumeInstancesCommute : Lean.ParserDescr

Equations

• Qq.doElemAssumeInstancesCommute = Lean.ParserDescr.node `Qq.doElemAssumeInstancesCommute 1024 (Lean.ParserDescr.symbol "assumeInstancesCommute")