Skip to content
scrambled
Programming Language Theory Concept

Intro pattern

Books JourneyProgramming Language Theory Statuslearning Tags
  • formal system
  • language feature design
  • proof reason technique
  • semantics
  • syntax grammar

[Rocq] A tactic modifier in Rocq:(/programming-language-theory/concepts/rocq) that destructures hypothesises as they're introduced (like intros [x y] to unpack a pair or intros [H|H] for a disjunction).