Value declaration with patterns on the left

[gisellemnr]

Currently we need to unpack all variables on the left of an SML declaration and create one Coq definition for each, duplicating some code. The SML code val x :: l = [1 ,2 ,3] becomes:

Definition x := match [1; 2; 3] with (x :: l) => x
                                   | _ => patternFailure
                end .
Definition l := match [1; 2; 3] with (x :: l) => l
                                   | _ => patternFailure
                end .

To avoid this duplication, we could use tuples:

Definition t := match [1; 2; 3] with (x :: l) => x
                                   | _ => patternFailure
                end .
Definition x := fst t.
Definition l := snd t.

Issues to solve when implementing this solution:

• Name for t should be unique.
• If the pattern has more than two variables, it is grouped (by Coq) ((1,2,3), 4). So fst returns another tuple. Depending on the index of the element, figure out how to organize fst and snd functions.