max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/compiler/erase_irrelevant): style

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-25 15:45:43 -07:00
parent be7a736a42
commit 1b8d9deb37
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/compiler/erase_irrelevant.cpp
View file

@ -113,7 +113,8 @@ class erase_irrelevant_fn : public compiler_step_visitor {
expr new_minor = minors[i];
for (unsigned j = 0; j < data_sz; j++) {
if (!is_lambda(new_minor))
throw exception("unexpected occurrence of 'cases_on' expression, the minor premise is expected to be a lambda-expression");
throw exception("unexpected occurrence of 'cases_on' expression, "
"the minor premise is expected to be a lambda-expression");
expr local = locals.push_local_from_binding(new_minor);
new_minor = instantiate(binding_body(new_minor), local);
}