From 2dbd529b499c2bb9dae754df0e449cad577ac7a0 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jul 2023 14:00:11 +0200
Subject: Add IList.lean

---
 backends/hol4/ilistScript.sml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'backends/hol4')

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 = [] ∧
 
-- 
cgit v1.2.3