Agda的目標類型中的`|是什麼意思？

Question

我在閱讀Brutal Meta-introduction to Agda。

在一節的「使用with和統一重寫」他們提了一個情況下的一種類型的目標從雲：

(filter p (a ∷ as) | p a) ≡ (filterN p (a ∷ as) | p a) 

到

(filter p (a ∷ rs) | r) ≡ (filterN p (a ∷ rs) | r) 

添加with子句之後。

我在編寫Agda代碼時看到類似的符號出現在目標和錯誤消息中。

我想知道，是否在|右邊有一個變量，在這個表示法中？這是記錄在任何地方？

Answer 1

如果你看一下定義過濾你看到的條款喜歡

... | true = a ∷ (filter p as) 

這對於

filter p (a ∷ as) | true = a ∷ (filter p as) 

的速記|目標中的符號指的是這些條款，這意味着例如

filter p (a ∷ as) | e 

當「e」等於「真」時等於「a∷（過濾器p）」。

在你的情況下，你有一個變量'r'，所以如果你的模式匹配，事情會計算更多。