diff options
Diffstat (limited to 'backends/lean/Base/IList')
| -rw-r--r-- | backends/lean/Base/IList/IList.lean | 8 |
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 α := |