News for hackers. Stuff that matters.

A comment on The limits of type theory: computation vs. interaction. Parent comment

Re:The limits of type theory: computation vs. interaction by murbard2 on Monday June 08, 2015 @09:35AM (#9678908)
It's great to have an example, but could you add inline comments for those of us who aren't familiar with Agda's syntax?
[ Parent | on HN ]
Re:The limits of type theory: computation vs. interaction by Retra on Monday June 08, 2015 @11:57AM (#9679893)
It's basically Haskell with unicode identifiers and mixed-fixity. (I.e., _::_ is an infix function of two arguments, and the _'s represent "holes" for the arguments.)
[ Parent | on HN ]