在类型声明中匹配Agda模式
在类型声明中匹配Agda模式
提问于 2020-03-06 04:09:58
我正在学习HoTT与Agda形式开始。我遵循了https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/中的说明
当我开始按指示输入依赖和类型归纳的声明时，
record Σ { } {X : ̇ } (Y : X → ̇ ) : ⊔ ̇ where
constructor _,_
field
x : X
y : Y x
pr₁ : {X : ̇ } {Y : X → ̇ } → Σ Y → X
pr₁ (x , y) = x
pr₂ : {X : ̇ } {Y : X → ̇ } → (z : Σ Y) → Y (pr₁ z)
pr₂ (x , y) = y
Σ-induction : {X : ̇ } {Y : X → ̇ } {A : Σ Y → ̇ }
→ ((x : X) (y : Y x) → A (x , y))
→ ((x , y) : Σ Y) → A (x , y)
Σ-induction g (x , y) = g x y我的agda说代码→ ((x , y) : Σ Y)有错误
expected sequence of possibly hidden bound identifiers当我更改类型声明时：
Σ-induction : {X : ̇ } {Y : X → ̇ } {A : Σ Y → ̇ }
→ ((x : X) (y : Y x) → A (x , y))
→ (z : Σ Y) → A (pr₁ z , pr₂ z)
Σ-induction g (x , y) = g x y这个版本没问题。
所以我想知道如果问题是agda不支持类型声明中的模式匹配。
附注：我正在使用Agda 2.6.0.1
回答 1
Stack Overflow用户
回答已采纳
发布于 2020-03-06 16:15:28
在望远镜记录上进行模式匹配的能力将在(不久)即将推出的Agda 2.6.1版本中提供。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/60557445
复制相关文章
相似问题
腾讯云开发者
