Concept

Tactic modifier

Modified just now

Journey Statuslearning Tags

Tools: Rocq (formerly Coq)

(Syntax & Grammar, Language feature/design) A syntactic addition to a Tactic that alters its behavior, such as intro patterns for intros or occurrence selectors for rewrite.