Merge pull request #240 from RaitoBezarius/has-int-pred

backends/lean: introduce `HasIntPred` automation

1 files changed, 5 insertions, 3 deletions

diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index a1897191..96843f55 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -18,9 +18,11 @@ theorem len_pos : 0 ≤ (ls : List α).len := by
   induction ls <;> simp [*]
   omega
 
-instance (a : Type u) : Arith.HasIntProp (List a) where
-  prop_ty := λ ls => 0 ≤ ls.len
-  prop := λ ls => ls.len_pos
+instance (l: List a) : Arith.HasIntPred (l.len) where
+   concl := 0 ≤ l.len
+   prop := l.len_pos
+
+example (l: List a): 0 ≤ l.len := by scalar_tac
 
 -- Remark: if i < 0, then the result is none
 def indexOpt (ls : List α) (i : Int) : Option α :=