当前位置: 首页> 房产> 建筑 > LEAN 类型理论之注解(Annotations of LEAN Type Theory)-- 商类型(Quotient Type)

LEAN 类型理论之注解(Annotations of LEAN Type Theory)-- 商类型(Quotient Type)

时间:2025/7/19 14:06:28来源:https://blog.csdn.net/sinat_36821938/article/details/141953130 浏览次数:0次

        商类型(Quotient Type),也称划分类型,通过给定义一个定义在某一类型 α 上的关系R:α → α→ ℙ,将类型α 中,满足关系R的元素摘出来,组成该商类型(Quotient),记 α / R。简单来说,有:

a,b : α,R a b ⊢ a,b : α / R

        如,定义在自然数(Nat)上的相等关系,即  α ≡ Nat,R ≡ Eq,有商类型 Nat / Eq,其元素包含所有自相等的自然数,即所有自然数,有 | Nat / Eq | = | Nat |。

        1. 类型规则(Type Formation Rule):

        2. 构建函数(Introduction Rule):        

       3. 使用函数(Eliminator Rule):

        4. 相等规则(Equality Rule):

        5. 步进规则(Progress Rule):

关键字:LEAN 类型理论之注解(Annotations of LEAN Type Theory)-- 商类型(Quotient Type)

版权声明:

本网仅为发布的内容提供存储空间,不对发表、转载的内容提供任何形式的保证。凡本网注明“来源:XXX网络”的作品,均转载自其它媒体,著作权归作者所有,商业转载请联系作者获得授权,非商业转载请注明出处。

我们尊重并感谢每一位作者,均已注明文章来源和作者。如因作品内容、版权或其它问题,请及时与我们联系,联系邮箱:809451989@qq.com,投稿邮箱:809451989@qq.com

责任编辑: