idris-lang/Idris-dev — pull request #1205 by david-christiansen (2014-05-06 18:25:13+00:00)
Title: Allow %name to take an infix name as an argument.

Fixes #1191.