[Lean] Advanced pattern-matching

[clementblaudeau]

Currently, the Lean backend only support "basic" pattern-matching : wild patterns, constructors, or-patterns. It should also support matching on:

• Arrays
• Constants
• Bindings with sub-patterns

Besides, it should prevent patterns on function arguments.

[abentkamp]

Array matching cannot be implemented in the Lean backend yet because of #804.
.

[abentkamp]

Re: Besides, it should prevent patterns on function arguments.
#1792