From 1f0e5b3cb80e9334b07bf4b074c01150f4abd49d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 22 May 2023 15:23:48 +0200
Subject: Make the unfolding theorems collection from evalLib persistent

---
 backends/hol4/divDefLibTestTheory.sig | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'backends/hol4/divDefLibTestTheory.sig')

diff --git a/backends/hol4/divDefLibTestTheory.sig b/backends/hol4/divDefLibTestTheory.sig
index 526f74a6..d8cc4ab5 100644
--- a/backends/hol4/divDefLibTestTheory.sig
+++ b/backends/hol4/divDefLibTestTheory.sig
@@ -13,6 +13,7 @@ sig
     val list_t_size_def : thm
     val node_TY_DEF : thm
     val node_case_def : thm
+    val nth0_def : thm
     val nth_def : thm
     val odd_def : thm
     val tree_TY_DEF : thm
@@ -180,6 +181,14 @@ sig
       
       ⊢ ∀a f. node_CASE (Node a) f = f a
    
+   [nth0_def]  Definition
+      
+      ⊢ ∀ls i.
+          nth0 ls i =
+          case ls of
+            ListCons x tl => if i = 0 then Return x else nth0 tl (i − 1)
+          | ListNil => Fail Failure
+   
    [nth_def]  Definition
       
       ⊢ ∀ls i.
-- 
cgit v1.2.3