equal
deleted
inserted
replaced
15 |
15 |
16 Ord_alt :: "i => o" |
16 Ord_alt :: "i => o" |
17 |
17 |
18 "**" :: "[i,i]=>i" (infixl 70) |
18 "**" :: "[i,i]=>i" (infixl 70) |
19 "++" :: "[i,i]=>i" (infixl 65) |
19 "++" :: "[i,i]=>i" (infixl 65) |
|
20 "--" :: "[i,i]=>i" (infixl 65) |
20 |
21 |
21 |
22 |
22 defs |
23 defs |
23 ordermap_def |
24 ordermap_def |
24 "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))" |
25 "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))" |
32 omult_def "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))" |
33 omult_def "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))" |
33 |
34 |
34 (*ordinal addition*) |
35 (*ordinal addition*) |
35 oadd_def "i ++ j == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))" |
36 oadd_def "i ++ j == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))" |
36 |
37 |
|
38 (*ordinal subtraction*) |
|
39 odiff_def "i -- j == ordertype(i-j, Memrel(i))" |
|
40 |
37 end |
41 end |