[Agda-dev] REWRITE rules

[Andreas Abel]

Hi Jesper [CC: agda-dev],

I added some initial description of rewriting to the coming release notes

   https://github.com/agda/agda/blob/maint-2.4.2/CHANGELOG

Some ideas:

1. We could allow several rewrite relations to be added with BUILTIN 
REWRITE.  After all, they only serve to specify to Agda how to recognize 
rewrite rules.

2. We could allow REWRITE pragmas even in the absence of --rewriting, 
but switch on rewriting during reduction only when option --rewriting is 
given.  This would allow to add rewrite rules to the standard library, 
but they would not be used unless the user declared that he wanted them.

3. In the long run, we have to thing about management of rewrite rules 
in imports.  The user should have some control over which rewrite rules 
he wants.  We could look into Isabelle how they do it there, for instance.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/