[Agda] «Extensionally but not definitionally equal» — can I say that?
kindaro at gmail.com
Sat Sep 3 11:46:11 CEST 2022
Suppose I have two definitions of addition — one works on Peano
numbers and the other works in binary representation. Can I express in
Agda that these two definitions are extensionally equal but
Ideally in the future I want to proceed to reasoning about their
asymptotic performance (linear versus logarithmic). So, I want to have
several notions of equality, finer than the commonly postulated
The way I imagine this could go is by reifying the definition of said
functions as a syntactic tree or another appropriate encoding of the
way Agda sees them. Then I should say «these two functions are
extensionally equal × their representation as syntactic trees is
distinct». Is this realistic? Are there other approaches?
See also on Zulip:
More information about the Agda