Dataset - CKAN

Implementation of three types of ordinals in Coq

One can define an inductive type T in Coq by the rules: zero is in T, and 'cons a n b' is in T when a, b are in T and n is an integer. One can embed this type with an...
- HTML

You can also access this registry using the API (see API Docs).