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

mwleeds / epigram

Automatically exported from code.google.com/p/epigram

0 stars 0 forks source link

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

Open GoogleCodeExporter opened 8 years ago

GoogleCodeExporter commented 8 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