This is a tiny Haskell "library" for generating comparators (equality and less than) for Agda data types.
Main.hs
contains an example for Agda's Term
and associated
types. The
generated output (along with two helper functions) can be found in
TermCmp.agda
.