Instances For
def
Lean.Compiler.LCNF.isTrivialConstructorApp?
(declName : Lake.Name)
(args : Array Lean.Compiler.LCNF.Arg)
:
Instances For
Instances For
def
Lean.Compiler.LCNF.ctorAppToMono
(ctorInfo : Lean.ConstructorVal)
(args : Array Lean.Compiler.LCNF.Arg)
:
Instances For
Instances For
partial def
Lean.Compiler.LCNF.decToMono
(c : Lean.Compiler.LCNF.Cases)
:
(c.typeName == `Decidable) = true → Lean.Compiler.LCNF.ToMonoM Lean.Compiler.LCNF.Code
partial def
Lean.Compiler.LCNF.trivialStructToMono
(info : Lean.Compiler.LCNF.TrivialStructureInfo)
(c : Lean.Compiler.LCNF.Cases)
:
Eliminate cases
for trivial structure. See hasTrivialStructure?