On 28/04/2015, at 11:36 PM, john skaller wrote:
> I'm giving up: I'm defining it directly in the compiler.
This now works:
fun f (x:int) : int => x + 1;
fun g (x:int): string => x.str+"!";
fun h (x:double) :string => x.str+"!";
var fgx = \prod (f,g,h);
println$ fgx (1,2,3.1);
On 28/04/2015, at 11:26 AM, john skaller wrote:
> However \prod (f,g,h) still can't be defined, i have ravel (f,g,h) in the
> library for up to 5 cases.
I'm giving up: I'm defining it directly in the compiler.
And sum too.
Now, to get the mediating morphism of a product, for many n,
we note t
This works:
fun \times[u1,u2,r1,r2] (f1:u1->r1,f2:u2->r2) : u1 * u2 -> r1 * r2 =>
fun (x1:u1,x2:u2) => f1 x1, f2 x2;
fun \otimes[D1,C1,D,C] (f1:(D1->C1), f:(D->C)) : (D1 ** D) -> (C1 ** C) =>
fun (a:D1 ** D) : C1 ** C => match a with
| (x1,,x) => f1 x1,,f x
endmatch
;
fun i2s (x:i
