It's great to have an example, but could you add inline comments for those of us... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		murbard2 on June 8, 2015 \| parent \| context \| favorite \| on: The limits of type theory: computation vs. interac... 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?

Retra on June 8, 2015 [–]

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.)

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact