noConfusion and unreachable patterns

[rambip]

In the chapter induction and recursion, part "dependant pattern matching", I find the explanations quite hard to follow.

First, the goal of the auxiliairy functions is not described explicitely
Worse, it uses "noConfusion". I was not able to find any documentation about this function, and no definition either.

I think it would be more clear to have a dedicated chapter about unreachable patterns explaining:

• what are the strategies to deal with unreachable patterns
• how does the equation compiler can understand some patterns are not accessible in a pattern matching
• how you ca use "False.elim" to fill impossible cases
• how to create a pattern matching with zero cases (or why it is impossible)
• what is the function "Nat.noConfusion"

An example to prove that 0 != 1 would be a nice illustation I think
I hope my feedback will help improve the documentation !

[rambip]

I found this explanation very helpfull:
https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/