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

fix: is_unsafe

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-30 12:03:55 -08:00
parent 1a8f79847d
commit 769debf970
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/declaration.cpp
View file

@ -262,7 +262,7 @@ bool constant_info::is_unsafe() const {
case constant_info_kind::Axiom: return to_axiom_val().is_unsafe();
case constant_info_kind::Definition: return to_definition_val().is_unsafe();
case constant_info_kind::Theorem: return false;
case constant_info_kind::Opaque: return false;
case constant_info_kind::Opaque: return to_opaque_val().is_unsafe();
case constant_info_kind::Quot: return false;
case constant_info_kind::Inductive: return to_inductive_val().is_unsafe();
case constant_info_kind::Constructor: return to_constructor_val().is_unsafe();

2
stage0/src/kernel/declaration.cpp
View file

@ -262,7 +262,7 @@ bool constant_info::is_unsafe() const {
case constant_info_kind::Axiom: return to_axiom_val().is_unsafe();
case constant_info_kind::Definition: return to_definition_val().is_unsafe();
case constant_info_kind::Theorem: return false;
case constant_info_kind::Opaque: return false;
case constant_info_kind::Opaque: return to_opaque_val().is_unsafe();
case constant_info_kind::Quot: return false;
case constant_info_kind::Inductive: return to_inductive_val().is_unsafe();
case constant_info_kind::Constructor: return to_constructor_val().is_unsafe();