# Documentation

Lean.Compiler.LCNF.Simp.DiscrM

• ctor:
• Natural numbers are morally constructor applications

natVal:
Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
• = match x with | => val.numParams | => 0
Equations
• One or more equations did not get rendered due to their size.
• A mapping from discriminant to constructor application it is equal to in the current context.

discrCtorMap :
• A mapping from constructor application to discriminant it is equal to in the current context.

ctorDiscrMap :
Instances For
@[inline]

Helper monad for tracking mappings from discriminant to constructor applications and back. The combinator withDiscrCtor should be used when visiting cases alternatives.

Equations

If fvarId is a constructor application, returns constructor information. Remark: we use the map discrCtorMap. Remark: We use this method when simplifying projections and cases-constructor.

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.

If type is an inductive datatype, return its universe levels and parameters.

Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.Compiler.LCNF.Simp.withDiscrCtorImp {α : Type} (discr : Lean.FVarId) (ctorName : Lean.Name) (ctorFields : ) :

Execute x with the information that discr = ctorName ctorFields. We use this information to simplify nested cases on the same discriminant.

Equations
def Lean.Compiler.LCNF.Simp.withDiscrCtorImp.updateCtx (discr : Lean.FVarId) (ctorName : Lean.Name) (ctorFields : ) :
Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.Compiler.LCNF.Simp.withDiscrCtor {m : TypeType u_1} {α : Type} [inst : ] (discr : Lean.FVarId) (ctorName : Lean.Name) (ctorFields : ) :
m αm α

Execute x with the information that discr = ctorName ctorFields. We use this information to simplify nested cases on the same discriminant.

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