sergei-romanenko / agda-hsubst-revised

Hereditary substitutions for simple types (revised)

Hereditary substitutions for simple types (revised)

Based on

1. Chantal Keller and Thorsten Altenkirch. 2010. Hereditary substitutions for simple types, formalized.
   In Proceedings of the third ACM SIGPLAN workshop on Mathematically structured functional programming (MSFP '10). ACM, New York, NY, USA, 3-10.
   DOI=10.1145/1863597.1863601
   http://doi.acm.org/10.1145/1863597.1863601

2. Chantal Keller. 2010. The decidability of the βη-equivalence using hereditary substitutions.
   http://www.lix.polytechnique.fr/~keller/Recherche/hsubst.html

I tried to refactor the code in [1] and [2], to make it more "good-looking". Whether the result is really better than the original, is disputable. "There's no accounting for taste." :-)

Note. [2] is under GNU General Public License. Thus, the part of the code that is based on [2] is under GPL. On the other hand, the text of the paper [1] is not under GPL. Hence, the code that is directly based on [1] needn't be under GPL (and it is not).