Ssreflect Users Discussion List

[Cyril <>]

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].

--
Cyril

On 27/09/2017 14:19, Nicolas Magaud wrote:
> Dear all,
>
> I have trouble defining finite functions (on finite domains) which have 2 or 
> more arguments using the [] notation.
> Below is a example of what I am trying to do.
>
> I would like to define the function f’ using pattern matching on a couple or 
> on the 2 separate arguments (in a currified way) but without doing explicit 
> lambda-abstraction.
>
> Is there a way to do that ? This would make the code more readable once the fun 
> and => keywords are gone.
>
> Nicolas Magaud
>
>
> (* full example *)
>
> Definition Symb := 'I_3.
>
> (* code that works *)
> Definition easy := [fun x : Symb => 0 with 0 |-> 16, 1 |-> 18, 2|-> 34].
>
> Definition f :=
>   [ fun x:Symb =>
>     [ fun y:Symb => 0 with
>     0 |-> [fun x':Symb => 17 with 0 |-> 42, 1 |-> 7, 2 |-> 28] x,
>     1 |-> [fun x':Symb => 34 with 0 |-> 2, 1 |-> 8, 2 |-> 70] x,
>     2 |-> [fun x':Symb => 72 with 0 |-> 116, 1 |-> 53, 2 |-> 47] x]].
>
> (* code I would like to write or something like that, i.e. with no 
> lambda-abstractions *)
> Definition f' :=
>    [fun (x,y) => 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].

--
Cyril