diff options
author | Son Ho | 2023-05-12 20:17:26 +0200 |
---|---|---|
committer | Son HO | 2023-06-04 21:54:38 +0200 |
commit | 8a5c5e4ae0cab0ab627c25ece59453a8e4bd4b64 (patch) | |
tree | 2e92885f457b610d183cf2e7f18fd05c5219ba60 /backends/hol4/testDivDefScript.sml | |
parent | c49fd4b6230a1f926e929f133794b6f73d338077 (diff) |
Cleanup the files of the HOL4 backend
Diffstat (limited to 'backends/hol4/testDivDefScript.sml')
-rw-r--r-- | backends/hol4/testDivDefScript.sml | 87 |
1 files changed, 0 insertions, 87 deletions
diff --git a/backends/hol4/testDivDefScript.sml b/backends/hol4/testDivDefScript.sml deleted file mode 100644 index 4a87895f..00000000 --- a/backends/hol4/testDivDefScript.sml +++ /dev/null @@ -1,87 +0,0 @@ -open HolKernel boolLib bossLib Parse -open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory - -open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory -open primitivesLib divDefLib - -val _ = new_theory "testDivDef" - -val def_qt = ‘ - (even (i : int) : bool result = - if i = 0 then Return T else odd (i - 1)) /\ - (odd (i : int) : bool result = - if i = 0 then Return F else even (i - 1)) -’ - -val even_def = DefineDiv def_qt - -(* Complexifying the above definition, and overriding on purpose *) -val def_qt = ‘ - (even (i : int) : bool result = - if i = 0 then - do - b <- Return T; - Return b - od - else do - b <- odd (i - 1); - Return b - od - ) /\ - (odd (i : int) : bool result = - if i = 0 then - do - b <- Return F; - Return b - od - else do - b <- even (i - 1); - Return b - od) -’ - -val even_def = DefineDiv def_qt - -Datatype: - list_t = - ListCons 't list_t - | ListNil -End - -val def_qt = ‘ - nth_mut_fwd (ls : 't list_t) (i : u32) : 't result = - case ls of - | ListCons x tl => - if u32_to_int i = (0:int) - then Return x - else - do - i0 <- u32_sub i (int_to_u32 1); - nth_mut_fwd tl i0 - od - | ListNil => - Fail Failure -’ - -val nth_mut_fwd_def = DefineDiv def_qt - -(* Complexifying the above definition, and overriding on purpose *) -val def_qt = ‘ - nth_mut_fwd (ls : 't list_t) (i : u32) : 't result = - case ls of - | ListCons x tl => - if u32_to_int i = (0:int) - then Return x - else - do - i0 <- u32_sub i (int_to_u32 1); - x <- nth_mut_fwd tl i0; - Return x - od - | ListNil => - Fail Failure -’ - -val nth_mut_fwd_def = DefineDiv def_qt - -val _ = export_theory () |