类型声明内的Agda模式匹配

Question

我正在以Agda形式学习HoTT。我按照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
我的阿格达说代码→ ((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不支持类型声明内的模式匹配。

ps.s。我正在使用Agda 2.6.0.1

我正在以Agda形式学习HoTT。我按照https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/中的说明进行操作，当我开始键入依赖和类型的声明时...

Answer 1

将在即将推出的版本Agda 2.6.1中提供望远镜中记录的模式匹配功能。

cf。开发分支的文档：https://agda.readthedocs.io/en/latest/language/telescopes.html#irrefutable-patterns-in-binding-positions