Showing changes from revision #3 to #4:
Added | Removed | Changed
The identity type has elements that are witnesses to the “sameness” of elements.
The identity type can be defined as the inductive type? with the following constructor: * for any, an element
Revision on October 10, 2018 at 13:43:01 by Ali Caglayan. See the history of this page for a list of all contributions to it.