在等价类上定义函数
Defining Functions on Equivalence Classes
摘要：
商构造从具体类型定义抽象类型，使用等价关系来标识具体类型中被视为不可区分的元素。商类型的元素是\emph{equivalence classes}：等价具体值的集合。简单的技术，提出了定义和推理商的建设，基于一个通用的引理库有关的功能，操作等价类。这些技术被应用到从自然数定义整数，然后定义一个递归的数据类型满足等式约束。
英文摘要：
A quotient construction defines an abstract type from a concrete type, using an equivalence relation to identify elements of the concrete type that are to be regarded as indistinguishable. The elements of a quotient type are \emph{equivalence classes}: sets of equivalent concrete values. Simple techniques are presented for defining and reasoning about quotient constructions, based on a general lemma library concerning functions that operate on equivalence classes. The techniques are applied to a definition of the integers from the natural numbers, and then to the definition of a recursive datatype satisfying equational constraints.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
