From e644419463072b8d1cdf2f16920d86a36a5a4040 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 15 May 2014 12:54:15 -0700
Subject: [PATCH] feat(library/bin_app): add simpler is_bin_app predicate

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/bin_app.cpp | 6 +++++-
 src/library/bin_app.h   | 2 ++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/library/bin_app.cpp b/src/library/bin_app.cpp
index 2c3f50ea1..8b04d60e3 100644
--- a/src/library/bin_app.cpp
+++ b/src/library/bin_app.cpp
@@ -7,8 +7,12 @@ Author: Leonardo de Moura
 #include "library/bin_app.h"
 
 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) {
-    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));
         rhs = app_arg(t);
         return true;
diff --git a/src/library/bin_app.h b/src/library/bin_app.h
index a6d408320..4c1943dbb 100644
--- a/src/library/bin_app.h
+++ b/src/library/bin_app.h
@@ -8,6 +8,8 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 
 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 */
 bool is_bin_app(expr const & t, expr const & f, expr & lhs, expr & rhs);