equal
deleted
inserted
replaced
22 |
22 |
23 fun mk_cnumeral 0 = @{cterm "Int.Pls"} |
23 fun mk_cnumeral 0 = @{cterm "Int.Pls"} |
24 | mk_cnumeral ~1 = @{cterm "Int.Min"} |
24 | mk_cnumeral ~1 = @{cterm "Int.Min"} |
25 | mk_cnumeral i = |
25 | mk_cnumeral i = |
26 let val (q, r) = Integer.div_mod i 2 in |
26 let val (q, r) = Integer.div_mod i 2 in |
27 Thm.capply (mk_cbit r) (mk_cnumeral q) |
27 Thm.apply (mk_cbit r) (mk_cnumeral q) |
28 end; |
28 end; |
29 |
29 |
30 |
30 |
31 (* number *) |
31 (* number *) |
32 |
32 |
45 |
45 |
46 in |
46 in |
47 |
47 |
48 fun mk_cnumber T 0 = instT T zeroT zero |
48 fun mk_cnumber T 0 = instT T zeroT zero |
49 | mk_cnumber T 1 = instT T oneT one |
49 | mk_cnumber T 1 = instT T oneT one |
50 | mk_cnumber T i = Thm.capply (instT T numberT number_of) (mk_cnumeral i); |
50 | mk_cnumber T i = Thm.apply (instT T numberT number_of) (mk_cnumeral i); |
51 |
51 |
52 end; |
52 end; |
53 |
53 |
54 |
54 |
55 (* code generator *) |
55 (* code generator *) |