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/divDefLibExampleScript.sml | |
parent | c49fd4b6230a1f926e929f133794b6f73d338077 (diff) |
Cleanup the files of the HOL4 backend
Diffstat (limited to '')
-rw-r--r-- | backends/hol4/divDefLibExampleScript.sml | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/backends/hol4/divDefLibExampleScript.sml b/backends/hol4/divDefLibExampleScript.sml new file mode 100644 index 00000000..c4a57783 --- /dev/null +++ b/backends/hol4/divDefLibExampleScript.sml @@ -0,0 +1,29 @@ +(* Examples which use divDefLib.DefineDiv *) + +open HolKernel boolLib bossLib Parse +open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory + +open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory +open primitivesLib +open divDefTheory divDefLib + +val [even_def, odd_def] = DefineDiv ‘ + (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 [nth_def] = DefineDiv ‘ + nth (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 tl i0 + od + | ListNil => Fail Failure +’ |