3 ms·
This seems to me like a less-formal (and consequently less powerful) implementation of type completion in dependent-type systems and theorem provers such as Agd
by whatgoodisaroad 10y ago
This seems to me like a less-formal (and consequently less powerful) implementation of type completion in dependent-type systems and theorem provers such as Agda or Coq.
- runeks 10y agoI believe you are correct. The advantage, on the other hand, is that you don't have to first acquire a PhD in mathematics and then learn Coq/Agda. Seriously though, simpler interfaces can add a lot of value, but only if the increase in ease of use makes up for the decrease in expressiveness.
- DanWaterworth 10y agoYou don't need a PhD to use dependent types. I don't have a Bachelor's.