Miscellaneous code actions #
This declares some basic tactic code actions, using the @[tactic_code_action]
API.
Return the syntax stack leading to target
from root
, if one exists.
Equations
Instances For
Constructs a hole with a kind matching the provided hole elaborator.
Equations
Instances For
Hole code action used to fill in a structure's field when specifying an instance.
In the following:
instance : Monad Id := _
invoking the hole code action "Generate a (minimal) skeleton for the structure under construction." produces:
instance : Monad Id where
pure := _
bind := _
and invoking "Generate a (maximal) skeleton for the structure under construction." produces:
instance : Monad Id where
map := _
mapConst := _
pure := _
seq := _
seqLeft := _
seqRight := _
bind := _
Equations
Instances For
Returns true if this field is an autoParam or optParam, or if it is given an optional value in a child struct.
Equations
Instances For
Invoking hole code action "Generate a list of equations for a recursive definition" in the following:
def foo : Expr → Unit := _
produces:
def foo : Expr → Unit := fun
| .bvar deBruijnIndex => _
| .fvar fvarId => _
| .mvar mvarId => _
| .sort u => _
| .const declName us => _
| .app fn arg => _
| .lam binderName binderType body binderInfo => _
| .forallE binderName binderType body binderInfo => _
| .letE declName type value body nonDep => _
| .lit _ => _
| .mdata data expr => _
| .proj typeName idx struct => _
Equations
Instances For
Invoking hole code action "Start a tactic proof" will fill in a hole with by done
.
Equations
Instances For
Similar to getElimExprInfo
, but returns the names of binders instead of just the numbers;
intended for code actions which need to name the binders.
Equations
Instances For
Finds the TermInfo
for an elaborated term stx
.
Equations
Instances For
Invoking tactic code action "Generate an explicit pattern match for 'induction'" in the following:
example (x : Nat) : x = x := by
induction x
produces:
example (x : Nat) : x = x := by
induction x with
| zero => sorry
| succ n ih => sorry
It also works for cases
.
Equations
Instances For
The "Add subgoals" code action puts · done
subgoals for any goals remaining at the end of a
proof.
example : True ∧ True := by
constructor
-- <- here
is transformed to
example : True ∧ True := by
constructor
· done
· done