canonical indeterminate forms for arrows
Closed this issue · 2 comments
I think there should be a fifth clause in this theorem because of the structure of the proof at https://github.com/hazelgrove/hazelnut-dynamics-agda/blob/master/canonical-indeterminate-forms.agda#L108 and https://github.com/hazelgrove/hazelnut-dynamics-agda/blob/master/canonical-indeterminate-forms.agda#L109 -- it's not exporting the full inversion of the rules involved, but something derived from them, unlike the others.
The d indet on this line should be d' indet:
(d indet holds trivially since its an assumption of the theorem)
Fixed in the 2/6 version of the notes.
Ah, good catch! That typo explains the weird "just return the whole second argument" thing, at least. I agree that the new version is more canonical, though.
The other thing that was happening is that I didn't notice I had a ⊥ in the context for one of the goals -- for matching to be exhaustive there's a case for TACast and ICastHoleGround, but unification gives you ⦇⦈ ground, which it isn't.
So with those two fixes, canonical-indeterminate-forms-hole now has exactly one case per summand in the output and is just pushing around variables, which is the "it's just inversion" invariant in Agda terminology.