Programming Language Theory ConceptTacticProperties 3Hide BooksChapter 1. Basics - functional programming in rocq JourneyProgramming Language Theory StatuslearningTools: Rocq (formerly Coq)INFO(Language feature/design, Formal system, Proof/Reason technique) A proof Command in Rocq that transforms the current Goal state, automating proof steps (like intros, apply, rewrite) to incrementally construct a proof term. Previous in ConceptsSystemNext in Concepts Tactic modifier