From a02fd7fb4cfac4c02d24a252352c8fdd85cfed4b Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 15 Aug 2018 09:10:11 -0700 Subject: [PATCH] feat(library/noncomputable): sorts are computable i.e. constant io.real_world : Type --- src/library/noncomputable.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp index 26f19940ae..8bddf1f869 100644 --- a/src/library/noncomputable.cpp +++ b/src/library/noncomputable.cpp @@ -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; }