equal
deleted
inserted
replaced
32 sfst_def "sfst == (LAM p.Isfst p)" |
32 sfst_def "sfst == (LAM p.Isfst p)" |
33 ssnd_def "ssnd == (LAM p.Issnd p)" |
33 ssnd_def "ssnd == (LAM p.Issnd p)" |
34 ssplit_def "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))" |
34 ssplit_def "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))" |
35 |
35 |
36 (* start 8bit 1 *) |
36 (* start 8bit 1 *) |
|
37 syntax |
|
38 "@Gstuple" :: "['a, args] => 'a ** 'b" ("(1É_,/ _Ê)") |
|
39 |
|
40 translations |
|
41 "Éx, y, zÊ" == "Éx, Éy, zÊÊ" |
|
42 "Éx, yÊ" == "(|x,y|)" |
37 (* end 8bit 1 *) |
43 (* end 8bit 1 *) |
38 |
44 |
39 end |
45 end |
40 |
46 |
41 |
47 |