search

google-code-export / omega

Automatically exported from code.google.com/p/omega
Other
2 stars 0 forks source link

easy to shoot in foot with theorem #44

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
What steps will reproduce the problem?
1. load <http://svn.berlios.de/svnroot/repos/al4nin/trunk/found-bugs/issue43-
SetEmulation.omg>
2. observe that file never gets loaded, loops forever

What is the expected output? What do you see instead?

Well, the behaviour is expected, but in case of divergent rewrite rules the 
user should get a 
warning at least.

It is understood that a powerful type system can produce divergent calculations 
at the type level.

Theorems of the form (Equal {stuff a} a) definitely should be permitted.

The testcase contains lots if noise, I try to clean up later.

Behaviour occurs (probably) with the Nov 8 snapshot, I  tested with a bunch of 
patches.

Original issue reported on code.google.com by ggr...@gmail.com on 12 Dec 2007 at 1:02

GoogleCodeExporter commented 9 years ago 
correction: that file should be

1. load <http://svn.berlios.de/svnroot/repos/al4nin/trunk/found-bugs/issue44-
SetEmulation.omg>

... of course.

Original comment by ggr...@gmail.com on 12 Dec 2007 at 1:07