equal
deleted
inserted
replaced
12 Arith = CTT + |
12 Arith = CTT + |
13 |
13 |
14 consts "#+","-","|-|" :: "[i,i]=>i" (infixr 65) |
14 consts "#+","-","|-|" :: "[i,i]=>i" (infixr 65) |
15 "#*",div,mod :: "[i,i]=>i" (infixr 70) |
15 "#*",div,mod :: "[i,i]=>i" (infixr 70) |
16 |
16 |
|
17 syntax (symbols) |
|
18 "op #*" :: [i, i] => i (infixr "#\\<times>" 70) |
|
19 |
|
20 syntax (HTML output) |
|
21 "op #*" :: [i, i] => i (infixr "#\\<times>" 70) |
|
22 |
17 rules |
23 rules |
18 add_def "a#+b == rec(a, b, %u v. succ(v))" |
24 add_def "a#+b == rec(a, b, %u v. succ(v))" |
19 diff_def "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))" |
25 diff_def "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))" |
20 absdiff_def "a|-|b == (a-b) #+ (b-a)" |
26 absdiff_def "a|-|b == (a-b) #+ (b-a)" |
21 mult_def "a#*b == rec(a, 0, %u v. b #+ v)" |
27 mult_def "a#*b == rec(a, 0, %u v. b #+ v)" |