Idris2/tests/idris2/docs001/input

:doc plus
:doc Nat
:doc List
:doc Show
:doc show
:doc Monad
:doc 1
:doc String
:doc Integer
:doc Bits16
:q
Initial implementation of :doc It's not pretty, but at least it exists now 2020-07-08 17:52:57 +03:00			`:doc plus`
			`:doc Nat`
			`:doc List`
			`:doc Show`
			`:doc show`
Extract interface info from hints 2020-07-08 19:21:28 +03:00			`:doc Monad`
Change :doc to use PTerm instead of Name (#1178) 2021-03-12 12:46:46 +03:00			`:doc 1`
[ more ] Hints for primitive types too! 2021-10-13 13:45:39 +03:00			`:doc String`
			`:doc Integer`
			`:doc Bits16`
Initial implementation of :doc It's not pretty, but at least it exists now 2020-07-08 17:52:57 +03:00			`:q`