idris-hackers/idris-mode — pull request #263 by david-christiansen (2014-10-30 05:15:50+00:00)
Title: Remove special support for _|_

Idris has renamed _|_ to "Void", so special commands and highlighting
are no longer necessary.

Fixes #259.