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

feat(library/bin_app): add simpler is_bin_app predicate

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-15 12:54:15 -07:00
parent 7c0cc3111a
commit e644419463
2 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/bin_app.cpp
View file

@ -7,8 +7,12 @@ Author: Leonardo de Moura
#include "library/bin_app.h" #include "library/bin_app.h"
namespace lean { namespace lean {
bool is_bin_app(expr const & t, expr const & f) {
return is_app(t) && is_app(app_fn(t)) && app_fn(app_fn(t)) == f;
}
bool is_bin_app(expr const & t, expr const & f, expr & lhs, expr & rhs) { bool is_bin_app(expr const & t, expr const & f, expr & lhs, expr & rhs) {
if (is_app(t) && is_app(app_fn(t)) && app_fn(app_fn(t)) == f) { if (is_bin_app(t, f)) {
lhs = app_arg(app_fn(t)); lhs = app_arg(app_fn(t));
rhs = app_arg(t); rhs = app_arg(t);
return true; return true;

2
src/library/bin_app.h
View file

@ -8,6 +8,8 @@ Author: Leonardo de Moura
#include "kernel/expr.h" #include "kernel/expr.h"
namespace lean { namespace lean {
/** \brief Return true iff \c t is of the form <tt>((f s1) s2)</tt> */
bool is_bin_app(expr const & t, expr const & f);
/** \brief Return true iff \c t is of the form <tt>((f s1) s2)</tt>, if the result is true, then store a1 -> lhs, a2 -> rhs */ /** \brief Return true iff \c t is of the form <tt>((f s1) s2)</tt>, if the result is true, then store a1 -> lhs, a2 -> rhs */
bool is_bin_app(expr const & t, expr const & f, expr & lhs, expr & rhs); bool is_bin_app(expr const & t, expr const & f, expr & lhs, expr & rhs);