Allow ommision of irrelevant terms in dependent types: X -> Y as degenerate Pi x:X.Y

sweirich / trellys

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

46 stars 6 forks source link

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago

Right now we have to write Pi x:X.Y, even if x is not free in Y.

Original issue reported on code.google.com by nathan.c...@gmail.com on 30 Dec 2010 at 2:55

GoogleCodeExporter commented 9 years ago

Original comment by nathan.c...@gmail.com on 30 Dec 2010 at 2:55

GoogleCodeExporter commented 9 years ago

See issue 9 https://code.google.com/p/trellys/issues/detail?id=9#c2

Original comment by nathan.c...@gmail.com on 31 Dec 2010 at 11:07

GoogleCodeExporter commented 9 years ago

Original comment by vilhelm....@gmail.com on 2 Jan 2011 at 10:09