while we are on this topic, можно спросить, какая разница между
data _==_ {A : Set} : A -> A -> Set where
refl : forall x -> x == x
и
data _==_ {A : Set} (x : A) : A -> Set where
refl : x == x
? (кроме формы конструктора, конечно; я имею в виду именно reasoning, который Агда сможет или не сможет выполнять? Или с этой т.з. совершенно всё равно?)
no subject
data _==_ {A : Set} : A -> A -> Set where refl : forall x -> x == x и data _==_ {A : Set} (x : A) : A -> Set where refl : x == x? (кроме формы конструктора, конечно; я имею в виду именно reasoning, который Агда сможет или не сможет выполнять? Или с этой т.з. совершенно всё равно?)