From 40471ca8e34059895869bcbd1cf6419f42110b02 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Mon, 10 Aug 2015 11:39:51 -0700
Subject: [PATCH] doc(frontends/lean/elaborator): assert invariant in visit_app

---
 src/frontends/lean/elaborator.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 5c1574792..23c12126e 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -662,8 +662,9 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) {
     if (!expl) {
         bool first = true;
         while (binding_info(f_type).is_strict_implicit() ||
-               (!first && binding_info(f_type).is_implicit()) ||
-               (!first && binding_info(f_type).is_inst_implicit())) {
+               binding_info(f_type).is_implicit() ||
+               binding_info(f_type).is_inst_implicit()) {
+            lean_assert(binding_info(f_type).is_strict_implicit() || !first);
             tag g          = f.get_tag();
             bool is_strict = true;
             bool inst_imp  = binding_info(f_type).is_inst_implicit();