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

mwleeds / epigram

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

0 stars 0 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