namme-anetten / epigram

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

Translation of StackError from DInTm to InTm #57

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago
Right now, in the definition of ProofState, we parameterise the StackError over 
any term representation: in ProofState.Edition.ProofState, we define 
ProofStateT.

Then, we have this disgusting code "lifting" errors from a |ProofStateT a| to a 
|ProofStateT b|. With issue #31 
(http://code.google.com/p/epigram/issues/detail?id=31), we are hoping to unify 
the error system, it would be could to see what we can do about the terms 
insides these errors.

Original issue reported on code.google.com by pedag...@gmail.com on 26 Aug 2010 at 4:06