Add more notation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
823fe6df07
commit
18f319d00f
1 changed files with 2 additions and 0 deletions
|
@ -14,8 +14,10 @@ namespace lean {
|
||||||
void init_builtin_notation(frontend & f) {
|
void init_builtin_notation(frontend & f) {
|
||||||
f.add_prefix("\u00ac", 40, const_name(mk_not_fn()));
|
f.add_prefix("\u00ac", 40, const_name(mk_not_fn()));
|
||||||
f.add_infixr("&&", 35, const_name(mk_and_fn()));
|
f.add_infixr("&&", 35, const_name(mk_and_fn()));
|
||||||
|
f.add_infixr("/\\", 35, const_name(mk_and_fn()));
|
||||||
f.add_infixr("\u2227", 35, const_name(mk_and_fn()));
|
f.add_infixr("\u2227", 35, const_name(mk_and_fn()));
|
||||||
f.add_infixr("||", 30, const_name(mk_or_fn()));
|
f.add_infixr("||", 30, const_name(mk_or_fn()));
|
||||||
|
f.add_infixr("\\/", 30, const_name(mk_or_fn()));
|
||||||
f.add_infixr("\u2228", 30, const_name(mk_or_fn()));
|
f.add_infixr("\u2228", 30, const_name(mk_or_fn()));
|
||||||
f.add_infixr("=>", 25, const_name(mk_implies_fn()));
|
f.add_infixr("=>", 25, const_name(mk_implies_fn()));
|
||||||
f.add_infixr("\u21D2", 25, const_name(mk_implies_fn()));
|
f.add_infixr("\u21D2", 25, const_name(mk_implies_fn()));
|
||||||
|
|
Loading…
Reference in a new issue