From 19bced702dc7c4230ec5de1c9551834ffd91c823 Mon Sep 17 00:00:00 2001 From: elsanussi-s-mneina <52800671+elsanussi-s-mneina@users.noreply.github.com> Date: Wed, 15 Jul 2020 09:50:19 -0400 Subject: [PATCH] fix typo: "lowercase later" to "lowercase letter" I think this is a spelling mistake. --- docs/source/updates/updates.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/updates/updates.rst b/docs/source/updates/updates.rst index 432a11fd8..024f50510 100644 --- a/docs/source/updates/updates.rst +++ b/docs/source/updates/updates.rst @@ -40,7 +40,7 @@ attempting to use an argument which is erased at run time. Erasure ------- -In Idris, names which begin with a lower case later are automatically bound +In Idris, names which begin with a lower case letter are automatically bound as implicit arguments in types, for example in the following skeleton definition, ``n``, ``a`` and ``m`` are implicitly bound: