[Agda] strange `case' requirement
mechvel at botik.ru
Sat Oct 26 11:48:55 CEST 2013
_∙u_ : Op₂ uC
(just x) ∙u (just y) = just (x ∙ y)
m ∙u nothing = m
nothing ∙u m = m
for uC = Maybe C, and a semigroup operation _∙u_ : Op₂ C
(this is extending a semigroup with unity represented as `nothing').
Then I prove
goal : (m : uC) → (nothing ∙u m) =u m
goal m = IsEquivalence.refl uEquiv
uSetoid = Data.Maybe.setoid setoid
uEquiv = Setoid.isEquivalence uSetoid
The report is
nothing ∙u .m != .m of type Maybe (Setoid.Carrier ......)
when checking that the expression uRefl has type
nothing ∙u .m =u .m
After several minutes I guess to try
goal nothing = uRefl
goal (just _) = uRefl,
It does work. But looks ugly.
1) Why is not the first version type-checked by normalization?
Is this by a fundamental reason, or by a confusion that can be improved
in further type checker?
2) Why m is dotted in the report, has this sense?
This is on Agda of darcs about August or September 2013.
More information about the Agda