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

chore(frontends/lean/builtin_cmds): handle FixedNoParam in the front-end

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-03 15:18:26 -08:00
parent fcf532ea67
commit 1fc7bbceb2
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/frontends/lean/builtin_cmds.cpp
View file

@ -715,9 +715,10 @@ static environment congr_cmd_core(parser & p, congr_kind kind) {
for (auto k : r->get_arg_kinds()) {
if (!first) out << ", "; else first = false;
switch (k) {
case congr_arg_kind::Fixed: out << "fixed"; break;
case congr_arg_kind::Eq: out << "eq"; break;
case congr_arg_kind::Cast: out << "cast"; break;
case congr_arg_kind::Fixed: out << "fixed"; break;
case congr_arg_kind::FixedNoParam: out << "fixed-noparm"; break;
case congr_arg_kind::Eq: out << "eq"; break;
case congr_arg_kind::Cast: out << "cast"; break;
}
}
out << "]\n";