| changeset 28562 | 4e74209f113e |
| parent 27823 | 52971512d1a2 |
| child 29012 | 9140227dc8c5 |
| 28561:056255ade52a | 28562:4e74209f113e |
|---|---|
35 |
35 |
36 definition |
36 definition |
37 [code inline]: "1 = Fin 1" |
37 [code inline]: "1 = Fin 1" |
38 |
38 |
39 definition |
39 definition |
40 [code inline, code func del]: "number_of k = Fin (number_of k)" |
40 [code inline, code del]: "number_of k = Fin (number_of k)" |
41 |
41 |
42 instance .. |
42 instance .. |
43 |
43 |
44 end |
44 end |
45 |
45 |