diff options
| author | Son Ho | 2023-05-22 15:23:48 +0200 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:54:38 +0200 |
| commit | 1f0e5b3cb80e9334b07bf4b074c01150f4abd49d (patch) | |
| tree | e66c708351b518bcda12bfa28ef3249eb3714cdb /backends/hol4/divDefLibTestTheory.sig | |
| parent | 77d775ecea850576b24d097b402571889faa2a15 (diff) | |
Make the unfolding theorems collection from evalLib persistent
Diffstat (limited to 'backends/hol4/divDefLibTestTheory.sig')
| -rw-r--r-- | backends/hol4/divDefLibTestTheory.sig | 9 |
1 files changed, 9 insertions, 0 deletions
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. |