As far as I know, the issue is that
1. Agda elaborates pattern matching lambdas to new top-level definitions
with machine-generated names
2. Agda does not look into bodies of pattern matching functions when
checking definitional equality
Hence, Agda doesn't know that two pattern matching lambdas which look the
same in the source are equal.
People tolerate this limitation because we rarely rely on the rather
fragile intensional equality of functions. Instead we postulate function
extensionality when required.
If you'd like to have a bit more intensional function equality, you can use
top-level lemmas instead of pattern lambdas, like this
If you'd like to have as much as possible intensional function equality,
you need to write all of your functions in terms of eliminators, thereby
making all of your function bodies visible to Agda, as induction method
arguments to eliminators.
Post by Philip Wadler
Why does the attached not work? Is there a workaround, or a repair on the
horizon? Note particularly the "1" in the error message, which appears
spurious. Cheers, -- P
. \ Philip Wadler, Professor of Theoretical Computer Science,
. /\ School of Informatics, University of Edinburgh
. / \ and Senior Research Fellow, IOHK
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
Agda mailing list