Agda, абсурд в образцах

[deni_ok]

Оказывается, абсурдный образец не обязателен (хотя и часто полезен) при отсутствии допустимых образцов конструктора:

module AbsurdTest where

Comments

[sassa_nf]

да, забавно. выходит, id {⊥} имеет тело.