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

feat(library/util): add is_app_of helper function

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-13 13:33:30 -08:00
parent 723a9e227a
commit c19be9d9e7
2 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/util.cpp
View file

@ -21,6 +21,16 @@ Author: Leonardo de Moura
#include "library/projection.h"
namespace lean {
bool is_app_of(expr const & t, name const & f_name) {
expr const & fn = get_app_fn(t);
return is_constant(fn) && const_name(fn) == f_name;
}
bool is_app_of(expr const & t, name const & f_name, unsigned nargs) {
expr const & fn = get_app_fn(t);
return is_constant(fn) && const_name(fn) == f_name && get_app_num_args(t) == nargs;
}
bool is_standard(environment const & env) {
return env.prop_proof_irrel() && env.impredicative();
}

5
src/library/util.h
View file

@ -9,6 +9,11 @@ Author: Leonardo de Moura
#include "kernel/type_checker.h"
namespace lean {
/** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_k) */
bool is_app_of(expr const & t, name const & f_name);
/** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_nargs) */
bool is_app_of(expr const & t, name const & f_name, unsigned nargs);
typedef std::unique_ptr<type_checker> type_checker_ptr;
/** \brief Unfold constant \c e or constant application (i.e., \c e is of the form (f ....),
where \c f is a constant */