search

mwleeds / epigram

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

Demo: ability to explicitly call the substEq simplifier run by Elim w/ motive #96

Open GoogleCodeExporter opened 8 years ago

GoogleCodeExporter commented 8 years ago 
In the definition of plusCommF in Plus.pig, there is a single call to substEq:

<= substEq Nat k1 k2 _ ;

The second equation is automatically simplified after elim w/ motive is 
executed. Actually, one can even solve the problem by calling the elimination 
on the identity eliminator:

<= id 

With id defined by:

make id := \ A a -> a : (A : Set) -> A -> A

One should be able to have our hand on the underlying simplification machinery, 
somehow.

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

GoogleCodeExporter commented 8 years ago 
Problem simplification doesn't currently introduce lambdas for foralls; if it 
did, this kind of thing would happen automatically. Is there any reason we 
wouldn't want to do this?

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