Ssreflect Users Discussion List

[Nicolas Magaud <>]

Thanks for this example.

This function has type : simpl_fun (prod_eqType nat_eqType nat_eqType) nat.

I have 2 other questions :

1/ Is it possible to have the type  "simpl_fun (prod_eqType ‘I_3 ‘I_3)" nat 
instead ?

2/ Moreover, is it possible to have a curryfing version of f’ whose type 
would be "simpl_fun ‘I_3 (simpl_fun ‘I_3 nat)" ?

Nicolas Magaud


> On 27 Sep 2017, at 15:09, Cyril 
> <>
>  wrote:
> 
> 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