idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-13 05:48:39 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #456 from chrrasmussen/patch-1

Browse Source 
Update reference to %auto_implicits in implementation notes
This commit is contained in:
Niklas Larsson 2020-07-13 11:53:01 +02:00 committed by GitHub
commit 7920eb8a0e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
docs/source/implementation/overview.rst
View File

@ -280,7 +280,7 @@ names, e.g. in:
... where ``xs`` is a ``Vect n a``, it infers bindings for ``n`` and ``a``.
The ``%auto_implicits`` directive means that it will no longer automatically
The ``%unbound_implicits`` directive means that it will no longer automatically
bind names (that is, ``a`` and ``b`` in ``map`` above) but it will still
infer the types for any additional names, e.g. if you write: