- ctor: Lean.ConstructorVal → Array Lean.Compiler.LCNF.Arg → Lean.Compiler.LCNF.Simp.CtorInfo
- natVal: Nat → Lean.Compiler.LCNF.Simp.CtorInfo
Natural numbers are morally constructor applications
Instances For
Equations
- (Lean.Compiler.LCNF.Simp.CtorInfo.ctor val args).getName = val.name
- (Lean.Compiler.LCNF.Simp.CtorInfo.natVal 0).getName = `Nat.zero
- (Lean.Compiler.LCNF.Simp.CtorInfo.natVal n).getName = `Nat.succ
Instances For
Equations
- (Lean.Compiler.LCNF.Simp.CtorInfo.ctor val args).getNumParams = val.numParams
- (Lean.Compiler.LCNF.Simp.CtorInfo.natVal n).getNumParams = 0
Instances For
Equations
- (Lean.Compiler.LCNF.Simp.CtorInfo.ctor val args).getNumFields = val.numFields
- (Lean.Compiler.LCNF.Simp.CtorInfo.natVal 0).getNumFields = 0
- (Lean.Compiler.LCNF.Simp.CtorInfo.natVal n).getNumFields = 1
Instances For
- discrCtorMap : Lean.FVarIdMap Lean.Compiler.LCNF.Simp.CtorInfo
A mapping from discriminant to constructor application it is equal to in the current context.
- ctorDiscrMap : Lean.PersistentExprMap Lean.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
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
Execute x
with the information that discr = ctorName ctorFields
.
We use this information to simplify nested cases on the same discriminant.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Execute x
with the information that discr = ctorName ctorFields
.
We use this information to simplify nested cases on the same discriminant.
Equations
- Lean.Compiler.LCNF.Simp.withDiscrCtor discr ctorName ctorFields = monadMap fun {β : Type} => Lean.Compiler.LCNF.Simp.withDiscrCtorImp discr ctorName ctorFields
Instances For
Equations
- One or more equations did not get rendered due to their size.