@@ -77,8 +77,15 @@ The available commands include:
77 Create a with-rule pattern match template for the clause of function ``NAME`` on line ``LINE``.
77 Create a with-rule pattern match template for the clause of function ``NAME`` on line ``LINE``.
78 The new code is returned with no highlighting.
78 The new code is returned with no highlighting.
80+ ``(:make-case LINE NAME)``
81+ Create a case pattern match template for the clause of function ``NAME`` on line ``LINE``.
82+ The new code is returned with no highlighting.
84+ ``(:make-lemma LINE NAME)``
85+ Create a top level function with a type which solves the hole named ``NAME`` on line ``LINE``.
80 ``(:proof-search LINE NAME HINTS)``
87 ``(:proof-search LINE NAME HINTS)``
81− Attempt to fill out the holes on ``LINE```named ``NAME`` by proof search.
88+ Attempt to fill out the holes on ``LINE`` named ``NAME`` by proof search.
82 ``HINTS`` is a possibly-empty list of additional things to try while searching.
89 ``HINTS`` is a possibly-empty list of additional things to try while searching.
84 ``(:docs-for NAME)``
91 ``(:docs-for NAME)``
@@ -111,6 +118,9 @@ The available commands include:
111 ``(:print-definition NAME)``
118 ``(:print-definition NAME)``
112 Return the definition of ``NAME`` as a highlighted string.
119 Return the definition of ``NAME`` as a highlighted string.
121+ ``(:repl-completions NAME)``
122+ Search names, types and documentations which contain ``NAME``.
114 ``(:version UID)``
124 ``(:version UID)``
115 Return the version information of the Idris compiler.
125 Return the version information of the Idris compiler.