hax icon indicating copy to clipboard operation
hax copied to clipboard
verified publisher icon hacspec

[Lean] Advanced pattern-matching

Open clementblaudeau opened this issue 3 months ago • 0 comments

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.

clementblaudeau avatar Sep 25 '25 15:09 clementblaudeau