From 18f319d00f07c52591e25dd3c425ef923549a833 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Aug 2013 10:43:55 -0700 Subject: [PATCH] Add more notation Signed-off-by: Leonardo de Moura --- src/frontend/builtin_notation.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/frontend/builtin_notation.cpp b/src/frontend/builtin_notation.cpp index dad1e5708..f36e3c1b5 100644 --- a/src/frontend/builtin_notation.cpp +++ b/src/frontend/builtin_notation.cpp @@ -14,8 +14,10 @@ namespace lean { void init_builtin_notation(frontend & f) { 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("\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("\u2228", 30, const_name(mk_or_fn())); f.add_infixr("=>", 25, const_name(mk_implies_fn())); f.add_infixr("\u21D2", 25, const_name(mk_implies_fn()));