mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-18 08:42:11 +03:00
Merge pull request #467 from elsanussi-s-mneina/patch-1
fix typo: "lowercase later" to "lowercase letter"
This commit is contained in:
commit
fd9de745ae
@ -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:
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user