search

mwleeds / epigram

Automatically exported from code.google.com/p/epigram
0 stars 0 forks source link

Demo: rename 'define' and 'relabel' to 'refine' #98

Closed GoogleCodeExporter closed 8 years ago

GoogleCodeExporter commented 8 years ago 
(I don't know if it's possible to do that with our stuffy parser)

Spectators were confused by the existence of 'define' and 'relabel' doing 
essentially the same thing. Maybe we could use a single name for this command, 
disambiguating its usage based on the presence of ':=' or not.

Original issue reported on code.google.com by pedag...@gmail.com on 7 Sep 2010 at 3:40

GoogleCodeExporter commented 8 years ago 
Done, though refine uses = rather than := since we can now make = a keyword 
while still keeping it as the name of a tactic.

http://www.e-pig.org/darcsweb/darcsweb?r=Pig09;a=commit;h=20100909125143-e29d1-3
ca0f0defb0809461d8c9dfe86bdfa0acebfab2c.gz

Original comment by adamgundry on 9 Sep 2010 at 2:55