types
('a, 'b) "ë" (infixr 5)
syntax
"Ú" :: "['a::{}, 'a] => prop" ("(_ Ú/ _)" [3, 2] 2)
"êë" :: "[prop, prop] => prop" ("(_ êë/ _)" [2, 1] 1)
"Gbigimpl" :: "[asms, prop] => prop" ("((3Ë _ Ì) êë/ _)" [0, 1] 1)
"Gall" :: "('a => prop) => prop" (binder "Ä" 0)
"Glam" :: "[idts, 'a::logic] => 'b::logic" ("(3³_./ _)" 10)
"Û" :: "['a, 'a] => bool" (infixl 50)
"Gnot" :: "bool => bool" ("¿ _" [40] 40)
"GEps" :: "[pttrn, bool] => 'a" ("(3®_./ _)" 10)
"GAll" :: "[idts, bool] => bool" ("(3Â_./ _)" 10)
"GEx" :: "[idts, bool] => bool" ("(3Ã_./ _)" 10)
"GEx1" :: "[idts, bool] => bool" ("(3Ã!_./ _)" 10)
"À" :: "[bool, bool] => bool" (infixr 35)
"Á" :: "[bool, bool] => bool" (infixr 30)
"çè" :: "[bool, bool] => bool" (infixr 25)
translations
(type) "x ë y" == (type) "x => y"
(* "³x.t" => "%x.t" *)
"x Û y" == "x ~= y"
"¿ y" == "~y"
"®x.P" == "@x.P"
"Âx.P" == "! x. P"
"Ãx.P" == "? x. P"
"Ã!x.P" == "?! x. P"
"x À y" == "x & y"
"x Á y" == "x | y"
"x çè y" == "x --> y"