search

sanyaade-g2g-repos / grammatical-framework

Automatically exported from code.google.com/p/grammatical-framework
0 stars 0 forks source link

Both random and exhaustive generation hang if the abstract syntax uses dependent types #4

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
Currently both generators just ignore the dependent types. In this way they 
generate many trees but the change to generate tree that is correct with 
respect to the dependent types is very low. For the user it looks like there 
is an infinite loop

Original issue reported on code.google.com by kr.ange...@gmail.com on 30 Nov 2009 at 9:08

GoogleCodeExporter commented 9 years ago 
Now we have our own theorem prover which is capable of term generation with 
dependent types

Original comment by kr.ange...@gmail.com on 21 Oct 2010 at 9:59