search

mietek / epigram2

Mirror of Epigram 2, by Conor McBride, et al.
https://code.google.com/p/epigram
MIT License
47 stars 7 forks source link

"define" tactics: advanced matching? #52

Closed GoogleCodeExporter closed 8 years ago

GoogleCodeExporter commented 8 years ago 
(Feature request from our Supreme Leader)

In demo.pig for instance, we define max:

> let max (x : Nat)(y : Nat) : Nat ;
> <= compare x y ;

Now, the current goal is:

> \ x : Nat ->
> \ y : Nat ->
> Programming: < max^1 x (plus x ('suc y)) : Nat >

Is it possible to solve it by typing:

> define max x (plus x ('suc y)) = plus x ('suc y) ;

Or something similar?

Right now, the parser complains.

Original issue reported on code.google.com by pedag...@gmail.com on 25 Aug 2010 at 11:37

GoogleCodeExporter commented 8 years ago 
Fixed.

http://www.e-pig.org/darcsweb?r=Pig09;a=commit;h=20100913113112-e29d1-2283dca36a
b16a1291d83ce62422918be3a5f1e6.gz

Original comment by adamgundry on 21 Sep 2010 at 7:56