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

feat(library/noncomputable): sorts are computable

Browse source 
i.e.

constant io.real_world : Type
This commit is contained in:
Sebastian Ullrich 2018-08-15 09:10:11 -07:00 • committed by Leonardo de Moura
parent 6e3a6ff40f
commit a02fd7fb4c
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/noncomputable.cpp
View file

@ -77,7 +77,8 @@ static bool is_noncomputable(old_type_checker & tc, noncomputable_ext const & ex
if (d.is_meta()) {
return false; /* ignore nontrusted definitions */
} else if (d.is_axiom()) {
return !env.is_builtin(d.get_name()) && !tc.is_prop(d.get_type()) && !is_builtin_extra(d.get_name());
return !env.is_builtin(d.get_name()) && !tc.is_prop(d.get_type()) && !is_sort(d.get_type()) &&
!is_builtin_extra(d.get_name());
} else {
return false;
}