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

fix(library/vm/vm_environment) use is_structure rather than try to catch an assertion

Browse source
This commit is contained in:
Scott Morrison 2017-04-29 18:06:38 +10:00 • committed by Sebastian Ullrich
parent 41c648905e
commit 832c38d3cb
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/vm/vm_environment.cpp
View file

@ -218,9 +218,9 @@ vm_obj environment_is_namespace(vm_obj const & env, vm_obj const & n) {
}
vm_obj environment_structure_fields(vm_obj const & env, vm_obj const & n) {
try {
if (is_structure(to_env(env), to_name(n))) {
return mk_vm_some(to_obj(get_structure_fields(to_env(env), to_name(n))));
} catch (exception &) {
} else {
return mk_vm_none();
}
}