source
def Qq.termAssumeInstancesCommute'_ :
Lean.ParserDescr
Equations

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

Instances For

source
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.

Instances For

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

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

Instances For

source
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.

Instances For

source
def Qq.Impl.termAssertInstancesCommuteImpl_ :
Lean.ParserDescr
Equations

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

Instances For

source
def Qq.Impl.termAssertInstancesCommuteDummy :
Lean.ParserDescr
Equations

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

Instances For

source
def Qq.Impl.termAssumeInstancesCommuteDummy :
Lean.ParserDescr
Equations

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

Instances For

source
def Qq.doElemAssertInstancesCommute :
Lean.ParserDescr
Equations

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

Instances For

source
def Qq.doElemAssumeInstancesCommute :
Lean.ParserDescr
Equations

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

Instances For