Что означает `` `в типе цели в Агда?

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.

Я видел, что аналогичная запись отображается в сообщениях целей и ошибок при написании кода Агда.

Мне интересно, имеет ли смысл иметь переменную справа от |, в этом обозначении? Является ли это документированным где угодно?

Answer 1

Если посмотреть на определение для фильтра, который вы видите положения как

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

которые являются обобщающим для

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

| обозначение в целях относится к этим статьям, это означает, что, например,

filter p (a ∷ as) | e 

равно «в ∷ (фильтр) в качестве р», когда «е» равно «истина».

В вашем случае у вас есть переменная 'r', поэтому, если вы сопоставляете шаблон с ней, все будет вычисляться больше.