@@ -326,10 +326,14 @@ namespace Tactics
326 ||| the body. Requires that the hole be in binding form (use
326 ||| the body. Requires that the hole be in binding form (use
327 ||| `attack`).
327 ||| `attack`).
329− ||| @ n the name to use for the argument, or `Nothing` to use the name
329+ ||| @ n the name to use for the argument
330− ||| in the corresponding hole type (a dependent function)
330+ intro : (n : TTName) -> Elab ()
331+ intro n = prim__Intro (Just n)
333+ ||| Introduce a lambda binding around the current hole and focus on
334+ ||| the body, using the name provided by the type of the hole.
331− intro : (n : Maybe TTName) -> Elab ()
335+ intro' : Elab ()
332− intro n = prim__Intro n
336+ intro' = prim__Intro Nothing
334 ||| Introduce a dependent function type binding into the current hole,
338 ||| Introduce a dependent function type binding into the current hole,
335 ||| and focus on the body.
339 ||| and focus on the body.