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

fix(library/definitional/equations): memory access violation

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-07 17:06:41 -08:00
parent 597f7385e8
commit 5c118127ae
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/definitional/equations.cpp
View file

@ -967,7 +967,8 @@ class equation_compiler_fn {
unsigned nindices = *inductive::get_num_indices(env(), const_name(I)); unsigned nindices = *inductive::get_num_indices(env(), const_name(I));
if (nindices > 0) { if (nindices > 0) {
buffer<expr> args; buffer<expr> args;
get_app_args(I, args); get_app_args(t, args);
lean_assert(args.size() >= nindices);
return return
all_distinct_locals(nindices, args.end() - nindices) && all_distinct_locals(nindices, args.end() - nindices) &&
std::all_of(args.end() - nindices, args.end(), std::all_of(args.end() - nindices, args.end(),