blob: c4a57783c2f16750ec3e1b2333ff5109d1fa6275 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
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
’
|
