Ssreflect Users Discussion List

[Nicolas Magaud <>]

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