@@ -183,27 +183,28 @@ namespace Tactics
183 fail : List ErrorReportPart -> Elab a
183 fail : List ErrorReportPart -> Elab a
184 fail err = prim__Fail err
184 fail err = prim__Fail err
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.
187 getEnv : Elab (List (TTName, Binder TT))
187 getEnv : Elab (List (TTName, Binder TT))
188 getEnv = prim__Env
188 getEnv = prim__Env
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.
191 getGoal : Elab (TTName, TT)
191 getGoal : Elab (TTName, TT)
192 getGoal = prim__Goal
192 getGoal = prim__Goal
194− ||| Get the hole queue, in order
194+ ||| Get the hole queue, in order.
195 getHoles : Elab (List TTName)
195 getHoles : Elab (List TTName)
196 getHoles = prim__Holes
196 getHoles = prim__Holes
198− ||| If the current hole contains a guess, return it
198+ ||| If the current hole contains a guess, return it. Otherwise, fail.
199 getGuess : Elab (Maybe TT)
199 getGuess : Elab (Maybe TT)
200 getGuess = prim__Guess
200 getGuess = prim__Guess
202− ||| Look up the types of every overloading of a name
202+ ||| Look up the types of every overloading of a name.
203 lookupTy : TTName -> Elab (List (TTName, NameType, TT))
203 lookupTy : TTName -> Elab (List (TTName, NameType, TT))
204 lookupTy n = prim__LookupTy n
204 lookupTy n = prim__LookupTy n
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.
207 lookupTyExact : TTName -> Elab (TTName, NameType, TT)
208 lookupTyExact : TTName -> Elab (TTName, NameType, TT)
208 lookupTyExact n = case !(lookupTy n) of
209 lookupTyExact n = case !(lookupTy n) of
209 [res] => return res
210 [res] => return res
@@ -211,28 +212,29 @@ namespace Tactics
211 xs => fail [NamePart n, TextPart "is ambiguous."]
212 xs => fail [NamePart n, TextPart "is ambiguous."]
213 ||| Find the reflected representation of all datatypes whose names
214 ||| Find the reflected representation of all datatypes whose names
214− ||| are overloadings of some name
215+ ||| are overloadings of some name.
215 lookupDatatype : TTName -> Elab (List Datatype)
216 lookupDatatype : TTName -> Elab (List Datatype)
216 lookupDatatype n = prim__LookupDatatype n
217 lookupDatatype n = prim__LookupDatatype n
218 ||| Find the reflected representation of a datatype, given its
219 ||| 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
220 lookupDatatypeExact : TTName -> Elab Datatype
222 lookupDatatypeExact : TTName -> Elab Datatype
221 lookupDatatypeExact n = case !(lookupDatatype n) of
223 lookupDatatypeExact n = case !(lookupDatatype n) of
222 [res] => return res
224 [res] => return res
223 [] => fail [TextPart "No datatype named", NamePart n]
225 [] => fail [TextPart "No datatype named", NamePart n]
224 xs => fail [TextPart "More than one datatype named", NamePart n]
226 xs => fail [TextPart "More than one datatype named", NamePart n]
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.
227 check : (tm : Raw) -> Elab (TT, TT)
229 check : (tm : Raw) -> Elab (TT, TT)
228 check tm = prim__Check tm
230 check tm = prim__Check tm
230 ||| Convert a type-annotated reflected term to its untyped
232 ||| Convert a type-annotated reflected term to its untyped
231− ||| equivalent
233+ ||| equivalent.
232 forgetTypes : TT -> Elab Raw
234 forgetTypes : TT -> Elab Raw
233 forgetTypes tt = prim__Forget tt
235 forgetTypes tt = prim__Forget tt
235− ||| Get the goal type as a Raw term
237+ ||| Get the goal type as a Raw term. Fails if there are no holes.
236 goalType : Elab Raw
238 goalType : Elab Raw
237 goalType = do g <- getGoal
239 goalType = do g <- getGoal
238 forgetTypes (snd g)
240 forgetTypes (snd g)
@@ -249,7 +251,8 @@ namespace Tactics
249 solve : Elab ()
251 solve : Elab ()
250 solve = prim__Solve
252 solve = prim__Solve
252− ||| Place a term into a hole, unifying its type
254+ ||| Place a term into a hole, unifying its type. Fails if the focus
253 fill : Raw -> Elab ()
256 fill : Raw -> Elab ()
254 fill tm = prim__Fill tm
257 fill tm = prim__Fill tm
@@ -297,7 +300,8 @@ namespace Tactics
297 Elab (List (TTName, TTName))
300 Elab (List (TTName, TTName))
298 matchApply tm argSpec = prim__Apply tm argSpec
301 matchApply tm argSpec = prim__Apply tm argSpec
300− ||| Move the focus to the specified hole
303+ ||| Move the focus to the specified hole. Fails if the hole does not
302 ||| @ hole the hole to focus on
306 ||| @ hole the hole to focus on
303 focus : (hole : TTName) -> Elab ()
307 focus : (hole : TTName) -> Elab ()
@@ -308,7 +312,9 @@ namespace Tactics
308 unfocus : TTName -> Elab ()
312 unfocus : TTName -> Elab ()
309 unfocus hole = prim__Unfocus hole
313 unfocus hole = prim__Unfocus hole
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
313 ||| The binding tactics require that a hole be directly under its
319 ||| The binding tactics require that a hole be directly under its
314 ||| binding, or else the scopes of the generated terms won't make
320 ||| binding, or else the scopes of the generated terms won't make
@@ -320,7 +326,8 @@ namespace Tactics
320 ||| Introduce a new hole with a specified name and type.
326 ||| Introduce a new hole with a specified name and type.
322 ||| The new hole will be focused, and the previously-focused hole
328 ||| 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.
324 claim : TTName -> Raw -> Elab ()
331 claim : TTName -> Raw -> Elab ()
325 claim n ty = prim__Claim n ty
332 claim n ty = prim__Claim n ty
@@ -333,12 +340,19 @@ namespace Tactics
333 intro n = prim__Intro (Just n)
340 intro n = prim__Intro (Just n)
335 ||| Introduce a lambda binding around the current hole and focus on
342 ||| 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
346+ ||| Requires that the hole be immediately under its binder (use
347+ ||| `attack` if it might not be).
337 intro' : Elab ()
348 intro' : Elab ()
338 intro' = prim__Intro Nothing
349 intro' = prim__Intro Nothing
340 ||| Introduce a dependent function type binding into the current hole,
351 ||| Introduce a dependent function type binding into the current hole,
341 ||| and focus on the body.
352 ||| and focus on the body.
354+ ||| Requires that the hole be immediately under its binder (use
355+ ||| `attack` if it might not be).
342 forall : TTName -> Raw -> Elab ()
356 forall : TTName -> Raw -> Elab ()
343 forall n ty = prim__Forall n ty
357 forall n ty = prim__Forall n ty
@@ -347,10 +361,16 @@ namespace Tactics
347 patvar n = prim__PatVar n
361 patvar n = prim__PatVar n
349 ||| Introduce a new pattern binding.
363 ||| Introduce a new pattern binding.
365+ ||| Requires that the hole be immediately under its binder (use
366+ ||| `attack` if it might not be).
350 patbind : TTName -> Elab ()
367 patbind : TTName -> Elab ()
351 patbind n = prim__PatBind n
368 patbind n = prim__PatBind n
353− ||| Introduce a new let binding
370+ ||| Introduce a new let binding.
372+ ||| Requires that the hole be immediately under its binder (use
373+ ||| `attack` if it might not be).
355 ||| @ n the name to let bind
375 ||| @ n the name to let bind
356 ||| @ ty the type of the term to be let-bound
376 ||| @ ty the type of the term to be let-bound
@@ -415,6 +435,10 @@ namespace Tactics
415 ||| constructs a context for `replace` using them. In some cases,
435 ||| constructs a context for `replace` using them. In some cases,
416 ||| this is not possible, and `replace` must be called manually with
436 ||| this is not possible, and `replace` must be called manually with
417 ||| an appropriate context.
437 ||| an appropriate context.
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).
418 rewriteWith : Raw -> Elab ()
442 rewriteWith : Raw -> Elab ()
419 rewriteWith rule = prim__Rewrite rule
443 rewriteWith rule = prim__Rewrite rule