idris-lang/Idris-dev — pull request #1208 by david-christiansen (2014-05-07 08:57:15+00:00)
Title: Docs for primitives

Allow primitive types to be entered into :doc. Also add their documentation to IDESlave annotations. This stops `:doc String` from throwing an error, and it makes IDEs nicer to use.