Agda不允许我用匹配类型的项填充类型空洞,因为存在定义上的相等约束。
创始人
2024-07-30 19:30:45
0

Agda不允许使用匹配类型的项填充类型空洞,因为在类型空洞中可能存在定义上的相等约束。相等约束是指在类型空洞中使用了可以在运行时进行比较的项,这会导致类型检查器无法确定该项的具体类型。为了解决这个问题,可以使用Agda的“with”表达式来处理匹配类型的情况。下面是一个示例代码:

open import Data.Empty
open import Data.Nat

data Even : ℕ → Set where
  even-zero : Even 0
  even-suc  : {n : ℕ} → Even n → Even (suc (suc n))

data Odd : ℕ → Set where
  odd-one  : Odd 1
  odd-suc  : {n : ℕ} → Odd n → Odd (suc (suc n))

even-or-odd : (n : ℕ) → Even n ⊎ Odd n
even-or-odd zero = inj₁ even-zero
even-or-odd (suc zero) = inj₂ odd-one
even-or-odd (suc (suc n)) with even-or-odd n
... | inj₁ ev = inj₂ (odd-suc ev)
... | inj₂ od = inj₁ (even-suc od)

在这个例子中,我们定义了两个归纳类型EvenOdd,它们表示自然数的偶数和奇数。然后我们定义了一个函数even-or-odd,它接受一个自然数作为参数,并返回一个Even n类型或Odd n类型的证明。在函数的定义中,我们使用了with表达式来处理匹配类型的情况。当我们在suc (suc n)上调用even-or-odd时,我们通过使用even-or-odd n来进行模式匹配,从而使用先前的证明构造新的证明。

使用with表达式可以避免使用匹配类型的项填充类型空洞时出现定义上的相等约束。相反,它允许我们根据已知的证明来构造新的证明,从而保证类型的一致性。

相关内容

热门资讯

安卓换鸿蒙系统会卡吗,体验流畅... 最近手机圈可是热闹非凡呢!不少安卓用户都在议论纷纷,说鸿蒙系统要来啦!那么,安卓手机换上鸿蒙系统后,...
app安卓系统登录不了,解锁登... 最近是不是你也遇到了这样的烦恼:手机里那个心爱的APP,突然就登录不上了?别急,让我来帮你一步步排查...
安卓系统拦截短信在哪,安卓系统... 你是不是也遇到了这种情况:手机里突然冒出了很多垃圾短信,烦不胜烦?别急,今天就来教你怎么在安卓系统里...
安卓系统要维护多久,安卓系统维... 你有没有想过,你的安卓手机里那个陪伴你度过了无数日夜的安卓系统,它究竟要陪伴你多久呢?这个问题,估计...
windows官网系统多少钱 Windows官网系统价格一览:了解正版Windows的购买成本Windows 11官方价格解析微软...
安卓系统如何卸载app,轻松掌... 手机里的App越来越多,是不是感觉内存不够用了?别急,今天就来教你怎么轻松卸载安卓系统里的App,让...
怎么复制照片安卓系统,操作步骤... 亲爱的手机控们,是不是有时候想把自己的手机照片分享给朋友,或者备份到电脑上呢?别急,今天就来教你怎么...
安卓系统应用怎么重装,安卓应用... 手机里的安卓应用突然罢工了,是不是让你头疼不已?别急,今天就来手把手教你如何重装安卓系统应用,让你的...
iwatch怎么连接安卓系统,... 你有没有想过,那款时尚又实用的iWatch,竟然只能和iPhone好上好?别急,今天就来给你揭秘,怎...
iphone系统与安卓系统更新... 最近是不是你也遇到了这样的烦恼?手机更新系统总是失败,急得你团团转。别急,今天就来给你揭秘为什么iP...