10 Commits

Author	SHA1	Message	Date
Dong Tsing-hsuen	505224e9fc	[ typo ] Enum -> Range (#1099)	2021-02-22 10:05:08 +00:00
Denis Buzdalov	a1b624a3bc	Tiny fix of the formatting in the recently added documentation.	2020-12-08 08:56:38 +00:00
Ruslan Feizerahmanov	1dba32a0c4	[ doc ] new application syntax (#820)	2020-12-07 18:59:49 +00:00
Fangyi Zhou	df4c454f4e	Typo in updates.rst	2020-08-17 19:33:14 +01:00
elsanussi-s-mneina	19bced702d	fix typo: "lowercase later" to "lowercase letter" ... I think this is a spelling mistake.	2020-07-15 09:50:19 -04:00
Keller, Bryn	a5449d926e	Update docs to reflect changes to ipkg format	2020-06-05 22:14:16 -07:00
Boyd Stephen Smith Jr	38876800ca	Mention %access specifically ... (The first failure I got when trying to compile Idris 1.3.1 code with Idris2.)	2020-05-27 12:51:41 -05:00
Edwin Brady	9c5594223e	Small documentation updates	2020-05-25 01:02:07 +01:00
Edwin Brady	498421a236	All functions now need to be covering by default ... This has caught a couple of things in the Idris 2 code base itself. Some tests needed partial annotations too.	2020-05-24 19:58:20 +01:00
Edwin Brady	fd55e629ee	Copy more files over from Idris2	2020-05-20 11:23:04 +01:00