Documentation

Lean.Compiler.LCNF.ToMono

Instances For
@[inline]
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
partial def Lean.Compiler.LCNF.decToMono :
(c.typeName == Decidable) = true

Convert cases Decidable => Bool

Eliminate cases for trivial structure. See hasTrivialStructure?`

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