Add idris-proof-search to glossary

Author: yurrriq

src/Basics.lidr

@@ -201,8 +201,8 @@ simplification."
 
 (For simple proofs like this, you can call \gls{idris-add-clause} with the point
 on the name (\idr{testNextWeekday}) in the type signature and then call
-\el{idris-proof-search} (\el{M-RET p}) with the point on the resultant hole to
-have Idris solve the proof for you.)
+\gls{idris-proof-search} with the point on the resultant hole to have Idris
+solve the proof for you.)
 
 \todo[inline]{Verify the "main uses" claim.}
 

src/glossary.tex

@@ -76,6 +76,18 @@
   A prefix argument restricts loading to the current line.
 }
 
+\longnewglossaryentry{idris-proof-search}{
+  name=\el{idris-proof-search},
+  sort={idris-proof-search}
+}
+{
+  \el{(idris-proof-search &optional ARG)}
+
+  Invoke the proof search. A plain prefix argument causes the
+  command to prompt for hints and recursion depth, while a numeric
+  prefix argument sets the recursion depth directly.
+}
+
 \newglossaryentry{induction}
 {
   name=\sl{induction},