equal
deleted
inserted
replaced
21 |
21 |
22 translations |
22 translations |
23 "(|x, y, z|)" == "(|x, (|y, z|)|)" |
23 "(|x, y, z|)" == "(|x, (|y, z|)|)" |
24 "(|x, y|)" == "spair`x`y" |
24 "(|x, y|)" == "spair`x`y" |
25 |
25 |
26 syntax (symbols) |
|
27 "@stuple" :: "['a, args] => 'a ** 'b" ("(1\\<lparr>_,/ _\\<rparr>)") |
|
28 |
|
29 defs |
26 defs |
30 spair_def "spair == (LAM x y.Ispair x y)" |
27 spair_def "spair == (LAM x y.Ispair x y)" |
31 sfst_def "sfst == (LAM p.Isfst p)" |
28 sfst_def "sfst == (LAM p.Isfst p)" |
32 ssnd_def "ssnd == (LAM p.Issnd p)" |
29 ssnd_def "ssnd == (LAM p.Issnd p)" |
33 ssplit_def "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))" |
30 ssplit_def "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))" |