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

Fix warning produced by clang++

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-04 04:40:43 -07:00
parent 57c0c69872
commit 00bee9c96e
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/lean_pp.cpp
View file

@ -928,7 +928,7 @@ class pp_fn {
lean_assert(is_choice(e)); lean_assert(is_choice(e));
unsigned num = get_num_choices(e); unsigned num = get_num_choices(e);
format r_format; format r_format;
unsigned r_weight; unsigned r_weight = 0;
for (unsigned i = 0; i < num; i++) { for (unsigned i = 0; i < num; i++) {
if (i > 0) if (i > 0)
r_format += format{space(), format("|"), line()}; r_format += format{space(), format("|"), line()};