A mapping from discriminant to constructor application it is equal to in the current context.
- ctorDiscrMap : PersistentExprMap FVarId
A mapping from constructor application to discriminant it is equal to in the current context.
Instances For
Helper monad for tracking mappings from discriminant to constructor applications and back.
The combinator withDiscrCtor
should be used when visiting cases
alternatives.
Equations
Instances For
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
Instances For
Execute x
with the information that discr = ctorName ctorFields
.
We use this information to simplify nested cases on the same discriminant.
Equations
Instances For
Equations
Instances For
Execute x
with the information that discr = ctorName ctorFields
.
We use this information to simplify nested cases on the same discriminant.