Demo: problem simplification should hit 'give xf n' on plusS in Plus.pig

mietek / epigram2

Mirror of Epigram 2, by Conor McBride, et al.

https://code.google.com/p/epigram

MIT License

48 stars 7 forks source link

Demo: problem simplification should hit 'give xf n' on plusS in Plus.pig #95

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago

Here is the definition of plusS:

make plusS : :- ((k : Nat)(n : Nat) => plus k ('suc n) == (: Nat) ('suc (plus k 
n))) ;
lambda k, n ;
<= Nat.Ind k ;
give xf n ;

This last 'give' is annoying: could the pro(b/p)simp hit that? It also appears 
in plusComm.

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