Безаргументный конструктор короче, поэтому в большинстве случаев удобнее (так в стандартной библиотеке и сделано). Единственное исключение - хитрые случаи, полезно/хочется видеть аппликативную структуру refl. Сравни, например
uip : {A : Set} (x y : A) (p q : x ≡ y) → p ≡ q
uip x .x (refl .x) (refl .x) = refl (refl x)
и
uip' : {A : Set} (x y : A) (p q : x ≐ y) → p ≐ q
uip' x .x refl' refl' = refl'
Хотя в первом случае в правой части можно вместо точного выражения, которое нам дает Агси (C-c C-a), написать
uip : {A : Set} (x y : A) (p q : x ≡ y) → p ≡ q
uip x .x (refl .x) (refl .x) = refl _
(Это справа вообще всегда можно делать с refl, потому что понятно, что туда пропишется NF из типа.)
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Date: 2014-01-08 11:50 pm (UTC)uip : {A : Set} (x y : A) (p q : x ≡ y) → p ≡ q uip x .x (refl .x) (refl .x) = refl (refl x)иuip' : {A : Set} (x y : A) (p q : x ≐ y) → p ≐ q uip' x .x refl' refl' = refl'Хотя в первом случае в правой части можно вместо точного выражения, которое нам дает Агси (C-c C-a), написатьuip : {A : Set} (x y : A) (p q : x ≡ y) → p ≡ q uip x .x (refl .x) (refl .x) = refl _(Это справа вообще всегда можно делать с refl, потому что понятно, что туда пропишется NF из типа.)