diff options
Diffstat (limited to 'backends/hol4/divDefLibTestScript.sml')
| -rw-r--r-- | backends/hol4/divDefLibTestScript.sml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/backends/hol4/divDefLibTestScript.sml b/backends/hol4/divDefLibTestScript.sml index c4a57783..b1243065 100644 --- a/backends/hol4/divDefLibTestScript.sml +++ b/backends/hol4/divDefLibTestScript.sml @@ -8,12 +8,16 @@ 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)) + (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)) ’ +Datatype: + list_t = + ListCons 't list_t + | ListNil +End + val [nth_def] = DefineDiv ‘ nth (ls : 't list_t) (i : u32) : 't result = case ls of |