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

fix(library/resolve_macro): typo

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-24 17:40:39 -07:00
parent 603dafbaf7
commit d7436e600b
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/resolve_macro.cpp
View file

@ -131,9 +131,9 @@ public:
expr C2 = arg_types[2];
buffer<expr> R; // resolvent
if (!collect(C1, l, R, ctx))
throw_kernel_exception(env, "invalid resolve macro positive literal was not found", m);
throw_kernel_exception(env, "invalid resolve macro, positive literal was not found", m);
if (!collect(C2, not_l, R, ctx))
throw_kernel_exception(env, "invalid resolve macro neative literal was not found", m);
throw_kernel_exception(env, "invalid resolve macro, negative literal was not found", m);
return mk_bin_rop(g_or, g_false, R.size(), R.data());
}