Motivation: ensure the correct type `IRType` is inferred for definitions
such as
```
def f (n : UInt32) : UInt32 :=
if n == 0 then panic! "foo"
else n+1
```
@kha @dselsam: I added this notation because I am tired of writing
`[elem1, elem2, ...].toArray`. BTW, the new notation is based on the
one available in SML.
`csimp` assumes constructors and `casesOn` applications match. That
is, given `I.casesOn x ...`, then if `x` is an constructor, then it is
a constructor of the inductive datatype `I`.
The transformation `erase_irrelevant` was violating this property when
it mixes `Decidable` and `Bool`. We fix this issue by mapping
`Decidable.casesOn`, `Decidable.isTrue` and `Decidable.isFalse` to
`Bool.casesOn`, `Bool.true` and `Bool.false` respectively.
In Lean4, we will not generate non dependent recursors for inductive
predicates. The main goal is to make the shape of the automatically
generated recursors more uniform. The non uniform representation is
leftover from Lean2. In Lean2, we wanted to support different kernels
with different features. For example: we could create proof relevant
kernels, no impredicative universe, etc.
Recall that, in a kernel with an impredicative Prop and no proof
irrelevance, inductive predicates without dependent elimination are
weaker that inductive predicates with dependent elimination.
When proof irrelevance is enabled, we can generate the dependent
recursor from the non dependent one. Actually, the module drec.cpp
generates the dependent recursor.
Now, we only support one kind of kernel, and it doesn't make sense
anymore to generate non dependent recursors for inductive predicates.
This would only produce an unnecessary asymmetry on the inductive
datatype module.
Remark: we had to create non dependent recursors to help the elaborator.
This can be avoid if we improve the elaborator. I will do that in the
new elaborator implemented in Lean.
Remark: equation lemmas are broken for definitions that pattern match on
nested inductive datatypes. The problem is the super messy
`prove_eq_rec_invertible_aux` function. This function will not be needed
after I finish the new inductive datatype support in the kernel.
cc @kha
We need this procedure otherwise it takes forever to prove equation lemmas
for definitions such as:
```
def macros : name → option macro
| `lambda := some lambda_macro
| `intro_x := some intro_x_macro
| _ := none
```
We never experienced this problem in Lean3 because we used `name`
literals only occurred in patterns of *meta* definitions. So, no
equation lemma was generated.
@kha `def macros` was taking more than 1 second to elaborate on my
machine. It is now instantaneous.
