Demo: Overload IMP to ARR (etc.) in the Evidence language

mietek / epigram2

Mirror of Epigram 2, by Conor McBride, et al.

https://code.google.com/p/epigram

MIT License

47 stars 7 forks source link

Demo: Overload IMP to ARR (etc.) in the Evidence language #100

Open GoogleCodeExporter opened 8 years ago

GoogleCodeExporter commented 8 years ago

Because Prop and Set are distinct entities, we can afford to overload their 
constructors (types pushed in anyway). Hence, we would have Pi-types for 
Forall, etc.

Then, we get overloaded notation in the high-level language: '->' for 
implication, instead of '=>'.

Original issue reported on code.google.com by pedag...@gmail.com on 9 Sep 2010 at 1:11