idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 12:42:02 +03:00
Code Issues Projects Releases Wiki Activity

[ doc ] Add note about ExprSearch

Browse Source
This commit is contained in:
Greg Werbin 2021-11-02 22:37:17 -04:00
parent 4926ae3ab5
commit 778fac7a8f
No known key found for this signature in database
GPG Key ID: 86D213EEE4D6618C
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
docs/source/implementation/ide-protocol.rst
View File

@ -108,6 +108,7 @@ They are compatible with Version 1 and 2.0 of the protocol unless otherwise stat
``(:proof-search LINE NAME HINTS)`` ``(:proof-search LINE NAME HINTS)``
Attempt to fill out the holes on ``LINE`` named ``NAME`` by proof search. Attempt to fill out the holes on ``LINE`` named ``NAME`` by proof search.
``HINTS`` is a possibly-empty list of additional things to try while searching. ``HINTS`` is a possibly-empty list of additional things to try while searching.
This operation is also called ``ExprSearch`` in the Idris 2 API.
``(:docs-for NAME [MODE])`` ``(:docs-for NAME [MODE])``
Look up the documentation for ``NAME``, and return it as a highlighted string. Look up the documentation for ``NAME``, and return it as a highlighted string.