equal
deleted
inserted
replaced
26 Infty ("\<infinity>") |
26 Infty ("\<infinity>") |
27 |
27 |
28 instance inat :: "{ord, zero}" .. |
28 instance inat :: "{ord, zero}" .. |
29 |
29 |
30 definition |
30 definition |
31 iSuc :: "inat => inat" |
31 iSuc :: "inat => inat" where |
32 "iSuc i = (case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>)" |
32 "iSuc i = (case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>)" |
33 |
33 |
34 defs (overloaded) |
34 defs (overloaded) |
35 Zero_inat_def: "0 == Fin 0" |
35 Zero_inat_def: "0 == Fin 0" |
36 iless_def: "m < n == |
36 iless_def: "m < n == |