@@ -183,27 +183,28 @@ namespace Tactics
183183 fail : List ErrorReportPart -> Elab a
184184 fail err = prim__Fail err
185185
186− ||| Look up the lexical binding at the focused hole
186+ ||| Look up the lexical binding at the focused hole. Fails if no holes are present.
187187 getEnv : Elab (List (TTName, Binder TT))
188188 getEnv = prim__Env
189189
190− ||| Get the name and type of the focused hole
190+ ||| Get the name and type of the focused hole. Fails if not holes are present.
191191 getGoal : Elab (TTName, TT)
192192 getGoal = prim__Goal
193193
194− ||| Get the hole queue, in order
194+ ||| Get the hole queue, in order.
195195 getHoles : Elab (List TTName)
196196 getHoles = prim__Holes
197197
198− ||| If the current hole contains a guess, return it
198+ ||| If the current hole contains a guess, return it. Otherwise, fail.
199199 getGuess : Elab (Maybe TT)
200200 getGuess = prim__Guess
201201
202− ||| Look up the types of every overloading of a name
202+ ||| Look up the types of every overloading of a name.
203203 lookupTy : TTName -> Elab (List (TTName, NameType, TT))
204204 lookupTy n = prim__LookupTy n
205205
206− ||| Get the type of a fully-qualified name
206+ ||| Get the type of a fully-qualified name. Fail if it doesn not
207+ ||| resolve uniquely.
207208 lookupTyExact : TTName -> Elab (TTName, NameType, TT)
208209 lookupTyExact n = case !(lookupTy n) of
209210 [res] => return res
@@ -211,28 +212,29 @@ namespace Tactics
211212 xs => fail [NamePart n, TextPart "is ambiguous."]
212213
213214 ||| Find the reflected representation of all datatypes whose names
214− ||| are overloadings of some name
215+ ||| are overloadings of some name.
215216 lookupDatatype : TTName -> Elab (List Datatype)
216217 lookupDatatype n = prim__LookupDatatype n
217218
218219 ||| Find the reflected representation of a datatype, given its
219− ||| fully-qualified name.
220+ ||| fully-qualified name. Fail if the name does not uniquely resolve
221+ ||| to a datatype.
220222 lookupDatatypeExact : TTName -> Elab Datatype
221223 lookupDatatypeExact n = case !(lookupDatatype n) of
222224 [res] => return res
223225 [] => fail [TextPart "No datatype named", NamePart n]
224226 xs => fail [TextPart "More than one datatype named", NamePart n]
225227
226− ||| Attempt to type-check a term, getting back itself and its type
228+ ||| Attempt to type-check a term, getting back itself and its type.
227229 check : (tm : Raw) -> Elab (TT, TT)
228230 check tm = prim__Check tm
229231
230232 ||| Convert a type-annotated reflected term to its untyped
231− ||| equivalent
233+ ||| equivalent.
232234 forgetTypes : TT -> Elab Raw
233235 forgetTypes tt = prim__Forget tt
234236
235− ||| Get the goal type as a Raw term
237+ ||| Get the goal type as a Raw term. Fails if there are no holes.
236238 goalType : Elab Raw
237239 goalType = do g <- getGoal
238240 forgetTypes (snd g)
@@ -249,7 +251,8 @@ namespace Tactics
249251 solve : Elab ()
250252 solve = prim__Solve
251253
252− ||| Place a term into a hole, unifying its type
254+ ||| Place a term into a hole, unifying its type. Fails if the focus
255+ ||| is not a hole.
253256 fill : Raw -> Elab ()
254257 fill tm = prim__Fill tm
255258
@@ -297,7 +300,8 @@ namespace Tactics
297300 Elab (List (TTName, TTName))
298301 matchApply tm argSpec = prim__Apply tm argSpec
299302
300− ||| Move the focus to the specified hole
303+ ||| Move the focus to the specified hole. Fails if the hole does not
304+ ||| exist.
301305 |||
302306 ||| @ hole the hole to focus on
303307 focus : (hole : TTName) -> Elab ()
@@ -308,7 +312,9 @@ namespace Tactics
308312 unfocus : TTName -> Elab ()
309313 unfocus hole = prim__Unfocus hole
310314
311− ||| Convert a hole to make it suitable for bindings.
315+ ||| Convert a hole to make it suitable for bindings - that is,
316+ ||| transform it such that it has the form `?h : t . h` as opposed to
317+ ||| `?h : t . f h`.
312318 |||
313319 ||| The binding tactics require that a hole be directly under its
314320 ||| binding, or else the scopes of the generated terms won't make
@@ -320,7 +326,8 @@ namespace Tactics
320326 ||| Introduce a new hole with a specified name and type.
321327 |||
322328 ||| The new hole will be focused, and the previously-focused hole
323− ||| will be immediately after it in the hole queue.
329+ ||| will be immediately after it in the hole queue. Because this
330+ ||| tactic introduces a new binding, you may need to `attack` first.
324331 claim : TTName -> Raw -> Elab ()
325332 claim n ty = prim__Claim n ty
326333
@@ -333,12 +340,19 @@ namespace Tactics
333340 intro n = prim__Intro (Just n)
334341
335342 ||| Introduce a lambda binding around the current hole and focus on
336− ||| the body, using the name provided by the type of the hole.
343+ ||| the body, using the name provided by the type of the
344+ ||| hole.
345+ |||
346+ ||| Requires that the hole be immediately under its binder (use
347+ ||| `attack` if it might not be).
337348 intro' : Elab ()
338349 intro' = prim__Intro Nothing
339350
340351 ||| Introduce a dependent function type binding into the current hole,
341352 ||| and focus on the body.
353+ |||
354+ ||| Requires that the hole be immediately under its binder (use
355+ ||| `attack` if it might not be).
342356 forall : TTName -> Raw -> Elab ()
343357 forall n ty = prim__Forall n ty
344358
@@ -347,10 +361,16 @@ namespace Tactics
347361 patvar n = prim__PatVar n
348362
349363 ||| Introduce a new pattern binding.
364+ |||
365+ ||| Requires that the hole be immediately under its binder (use
366+ ||| `attack` if it might not be).
350367 patbind : TTName -> Elab ()
351368 patbind n = prim__PatBind n
352369
353− ||| Introduce a new let binding
370+ ||| Introduce a new let binding.
371+ |||
372+ ||| Requires that the hole be immediately under its binder (use
373+ ||| `attack` if it might not be).
354374 |||
355375 ||| @ n the name to let bind
356376 ||| @ ty the type of the term to be let-bound
@@ -415,6 +435,10 @@ namespace Tactics
415435 ||| constructs a context for `replace` using them. In some cases,
416436 ||| this is not possible, and `replace` must be called manually with
417437 ||| an appropriate context.
438+ |||
439+ ||| Because this tactic internally introduces a `let` binding, it
440+ ||| requires that the hole be immediately under its binder (use
441+ ||| `attack` if it might not be).
418442 rewriteWith : Raw -> Elab ()
419443 rewriteWith rule = prim__Rewrite rule
420444