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

feat(library/util): add dec_level auxiliary procedure

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-04 13:25:58 -08:00
parent 926c140e17
commit 98a856373d
2 changed files with 29 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/library/util.cpp
View file

@ -12,6 +12,30 @@ Author: Leonardo de Moura
#include "library/locals.h"
namespace lean {
optional<level> dec_level(level const & l) {
switch (kind(l)) {
case level_kind::Zero: case level_kind::Param: case level_kind::Global: case level_kind::Meta:
return none_level();
case level_kind::Succ:
return some_level(succ_of(l));
case level_kind::Max:
if (auto lhs = dec_level(max_lhs(l))) {
if (auto rhs = dec_level(max_rhs(l))) {
return some_level(mk_max(*lhs, *rhs));
}}
return none_level();
case level_kind::IMax:
// Remark: the following mk_max is not a typo. The following
// assertion justifies it.
if (auto lhs = dec_level(imax_lhs(l))) {
if (auto rhs = dec_level(imax_rhs(l))) {
return some_level(mk_max(*lhs, *rhs));
}}
return none_level();
}
lean_unreachable(); // LCOV_EXCL_LINE
}
/** \brief Return true if environment has a constructor named \c c that returns
an element of the inductive datatype named \c I, and \c c must have \c nparams parameters.
*/

5
src/library/util.h
View file

@ -11,6 +11,11 @@ Author: Leonardo de Moura
namespace lean {
typedef std::unique_ptr<type_checker> type_checker_ptr;
/** \brief Reduce (if possible) universe level by 1.
\pre is_not_zero(l)
*/
optional<level> dec_level(level const & l);
bool has_unit_decls(environment const & env);
bool has_eq_decls(environment const & env);
bool has_heq_decls(environment const & env);