[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hello, The ordinals up to epsilon zero are one of the fundamental notions in the ACL2 system. See for instance: <http://www.ccs.neu.edu/home/pete/pub/acl2-ordinal-arithmetic-acl2.pdf> Note that in the ACL2 representation of ordinals there is no limit constructor, it's all about powers of omega (the "finite rooted trees" that Vladimir was talking about). Freek
