diff options
| author | Son Ho | 2023-07-13 14:00:11 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-13 14:00:11 +0200 |
| commit | 2dbd529b499c2bb9dae754df0e449cad577ac7a0 (patch) | |
| tree | 72c1cfbc8d29443fc2d70fd3f0ebfbd315954483 /backends/hol4/ilistScript.sml | |
| parent | 6cc0279045d40231f1cce83f0edb7aada1e59d92 (diff) | |
Add IList.lean
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/ilistScript.sml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/backends/hol4/ilistScript.sml b/backends/hol4/ilistScript.sml index fb0c7688..2b465af3 100644 --- a/backends/hol4/ilistScript.sml +++ b/backends/hol4/ilistScript.sml @@ -23,6 +23,8 @@ val _ = BasicProvers.export_rewrites ["len_def"] Remark: we initially added the following case, so that we wouldn't need the premise [i < len ls] is [index_eq_EL]: “index (i : int) [] = EL (Num i) []” + + TODO: this can be simplified. See the Lean backend. *) val index_def = Define ‘ index (i : int) (x :: ls) = if i = 0 then x else (if 0 < i then index (i - 1) ls else ARB) @@ -44,6 +46,7 @@ Proof exfalso >> cooper_tac QED +(* TODO: this can be simplified. See the Lean backend. *) val update_def = Define ‘ update ([] : 'a list) (i : int) (y : 'a) : 'a list = [] ∧ |