|
1826
|
1 |
types
|
|
|
2 |
('a, 'b) "ë" (infixr 5)
|
|
|
3 |
|
|
|
4 |
syntax
|
|
|
5 |
"Ú" :: "['a::{}, 'a] => prop" ("(_ Ú/ _)" [3, 2] 2)
|
|
|
6 |
"êë" :: "[prop, prop] => prop" ("(_ êë/ _)" [2, 1] 1)
|
|
|
7 |
"Gbigimpl" :: "[asms, prop] => prop" ("((3Ë _ Ì) êë/ _)" [0, 1] 1)
|
|
|
8 |
"Gall" :: "('a => prop) => prop" (binder "Ä" 0)
|
|
|
9 |
|
|
|
10 |
"Glam" :: "[idts, 'a::logic] => 'b::logic" ("(3³_./ _)" 10)
|
|
|
11 |
"Û" :: "['a, 'a] => bool" (infixl 50)
|
|
|
12 |
"Gnot" :: "bool => bool" ("¿ _" [40] 40)
|
|
|
13 |
"GEps" :: "[pttrn, bool] => 'a" ("(3®_./ _)" 10)
|
|
|
14 |
"GAll" :: "[idts, bool] => bool" ("(3Â_./ _)" 10)
|
|
|
15 |
"GEx" :: "[idts, bool] => bool" ("(3Ã_./ _)" 10)
|
|
|
16 |
"GEx1" :: "[idts, bool] => bool" ("(3Ã!_./ _)" 10)
|
|
|
17 |
"À" :: "[bool, bool] => bool" (infixr 35)
|
|
|
18 |
"Á" :: "[bool, bool] => bool" (infixr 30)
|
|
|
19 |
"çè" :: "[bool, bool] => bool" (infixr 25)
|
|
|
20 |
|
|
|
21 |
translations
|
|
|
22 |
(type) "x ë y" == (type) "x => y"
|
|
|
23 |
|
|
|
24 |
(* "³x.t" => "%x.t" *)
|
|
|
25 |
|
|
|
26 |
"x Û y" == "x ~= y"
|
|
|
27 |
"¿ y" == "~y"
|
|
|
28 |
"®x.P" == "@x.P"
|
|
|
29 |
"Âx.P" == "! x. P"
|
|
|
30 |
"Ãx.P" == "? x. P"
|
|
|
31 |
"Ã!x.P" == "?! x. P"
|
|
|
32 |
"x À y" == "x & y"
|
|
|
33 |
"x Á y" == "x | y"
|
|
|
34 |
"x çè y" == "x --> y"
|