From c19be9d9e71732094b800590d8cc2308505f2a78 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Jan 2016 13:33:30 -0800 Subject: [PATCH] feat(library/util): add is_app_of helper function --- src/library/util.cpp | 10 ++++++++++ src/library/util.h | 5 +++++ 2 files changed, 15 insertions(+) diff --git a/src/library/util.cpp b/src/library/util.cpp index 4424e7607..d7c72dc06 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -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(); } diff --git a/src/library/util.h b/src/library/util.h index 8bd094476..3bc0d4c5e 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -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_ptr; /** \brief Unfold constant \c e or constant application (i.e., \c e is of the form (f ....), where \c f is a constant */