michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add comments for unicode symbols, fix a typo

Browse source
This commit is contained in:
Soonho Kong 2013-08-21 10:43:00 -07:00
parent ce470f57db
commit 3f40953efc
2 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/frontends/lean/lean_notation.cpp
View file

@ -12,16 +12,16 @@ namespace lean {
\brief Initialize builtin notation.
*/
void init_builtin_notation(frontend & f) {
f.add_prefix("\u00ac", 40, mk_not_fn());
f.add_infixr("&&", 35, mk_and_fn());
f.add_infixr("/\\", 35, mk_and_fn());
f.add_infixr("\u2227", 35, mk_and_fn());
f.add_infixr("||", 30, mk_or_fn());
f.add_infixr("\\/", 30, mk_or_fn());
f.add_infixr("\u2228", 30, mk_or_fn());
f.add_infixr("=>", 25, mk_implies_fn());
f.add_infixr("\u21D2", 25, mk_implies_fn());
f.add_infixr("<=>", 25, mk_iff_fn());
f.add_infixr("\u21D4", 25, mk_iff_fn());
f.add_prefix("\u00ac", 40, mk_not_fn()); // "¬"
f.add_infixr("&&", 35, mk_and_fn()); // "&&"
f.add_infixr("/\\", 35, mk_and_fn()); // "/\"
f.add_infixr("\u2227", 35, mk_and_fn()); // "∧"
f.add_infixr("||", 30, mk_or_fn()); // "||"
f.add_infixr("\\/", 30, mk_or_fn()); // "\/"
f.add_infixr("\u2228", 30, mk_or_fn()); // "∨"
f.add_infixr("=>", 25, mk_implies_fn()); // "=>"
f.add_infixr("\u21D2", 25, mk_implies_fn()); // "⇒"
f.add_infixr("<=>", 25, mk_iff_fn()); // "<=>"
f.add_infixr("\u21D4", 25, mk_iff_fn()); // "⇔"
}
}

2
src/frontends/lean/lean_operator_info.h
View file

@ -14,7 +14,7 @@ namespace lean {
/**
\brief Operator fixity.
Prefix: ID _
Infixl: _ ID _
Infix: _ ID _
Infixl: _ ID _ (left associative)
Infixr: _ ID _ (right associative)
Postfix: _ ID