Ssreflect Users Discussion List

[Assia Mahboubi <>]

Dear Nicolas,

To remove any possible ambiguity : a documented in the header of the eqtype.v
library, the syntax:

[fun x : T => e0 with a1 |-> e1, .., a_n |-> e_n]

is not exactly for pattern matching on inductive arguments: it can be used as
soon as T is an instance of eqtype, and unfolds to

fun x => if x == a1 then e1 else if x == a2 then x2  .... else e0

Kind regards,

assia


Le 27/09/2017 à 15:09, Cyril a écrit :
> Dear Nicolas, your code almost work, because there is no need for a pattern
> matching:
> 
> Definition f' :=
>   [fun _ => 0 with (0,0) |-> 42,
>                    (0,1) |-> 7,
>                    (0,2) |-> 28,
>                    (1,0) |-> 2,
>                    (1,1) |-> 8,
>                    (1,2) |-> 70,
>                    (2,0) |-> 116,
>                    (2,1) |-> 53,
>                    (2,2) |-> 47].
>