[Agda] Making ≡ proofs more manageable

[Mateusz Kowalczyk]

On 13/01/14 12:23, Andreas Abel wrote:
> Maybe you should post the complete code after all...
>


It does seem like the best idea. I'm linking the file in question at
[1]. The whole project is included in the repository so you should be
able to load it without a problem. The proof in question was the
commented-out ‘passoc’ but the identity proofs I'm currently
postulating have similar ugly forms.

Of course I'm welcome to any comments not directly related to the question.

[1]:
https://github.com/Fuuzetsu/agdoparsec/blob/master/src/Data/Agdoparsec/Internal/Types.agda#L138

--
Mateusz K.