14 spair :: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *) |
14 spair :: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *) |
15 sfst :: "('a**'b)->'a" |
15 sfst :: "('a**'b)->'a" |
16 ssnd :: "('a**'b)->'b" |
16 ssnd :: "('a**'b)->'b" |
17 ssplit :: "('a->'b->'c)->('a**'b)->'c" |
17 ssplit :: "('a->'b->'c)->('a**'b)->'c" |
18 |
18 |
19 syntax "@spair" :: "'a => 'b => ('a**'b)" ("_##_" [101,100] 100) |
19 syntax |
|
20 "@stuple" :: "['a, args] => 'a ** 'b" ("(1'(|_,/ _|'))") |
20 |
21 |
21 translations "x##y" == "spair[x][y]" |
22 translations |
|
23 "(|x, y, z|)" == "(|x, (|y, z|)|)" |
|
24 "(|x, y|)" == "spair`x`y" |
22 |
25 |
23 rules |
26 rules |
24 |
27 |
25 inst_sprod_pcpo "(UU::'a**'b) = Ispair(UU,UU)" |
28 inst_sprod_pcpo "(UU::'a**'b) = Ispair UU UU" |
26 spair_def "spair == (LAM x y.Ispair(x,y))" |
29 |
27 sfst_def "sfst == (LAM p.Isfst(p))" |
30 defs |
28 ssnd_def "ssnd == (LAM p.Issnd(p))" |
31 spair_def "spair == (LAM x y.Ispair x y)" |
29 ssplit_def "ssplit == (LAM f. strictify[LAM p.f[sfst[p]][ssnd[p]]])" |
32 sfst_def "sfst == (LAM p.Isfst p)" |
|
33 ssnd_def "ssnd == (LAM p.Issnd p)" |
|
34 ssplit_def "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))" |
30 |
35 |
31 end |
36 end |
32 |
37 |
33 |
38 |
34 |
39 |