equal
deleted
inserted
replaced
12 Some basic definitions of ordinal numbers. Draws an Agda |
12 Some basic definitions of ordinal numbers. Draws an Agda |
13 development (in Martin-L\"of type theory) by Peter Hancock (see |
13 development (in Martin-L\"of type theory) by Peter Hancock (see |
14 @{url "http://www.dcs.ed.ac.uk/home/pgh/chat.html"}). |
14 @{url "http://www.dcs.ed.ac.uk/home/pgh/chat.html"}). |
15 *} |
15 *} |
16 |
16 |
17 datatype ordinal = |
17 datatype_new ordinal = |
18 Zero |
18 Zero |
19 | Succ ordinal |
19 | Succ ordinal |
20 | Limit "nat => ordinal" |
20 | Limit "nat => ordinal" |
21 |
21 |
22 primrec pred :: "ordinal => nat => ordinal option" |
22 primrec pred :: "ordinal => nat => ordinal option" |