scrambled
scrambled
Concept

Proof by case analysis

Modified just now
Books JourneyProgramming Language Theory Statuslearning Tags
  • formal system
  • language-feature-design
  • logic
  • programming paradigm
  • proof-reason-technique

Tools: Rocq (formerly Coq)

  • (Proof/Reason technique, Logic) A Proof technique that considers all possible forms of a value or Proposition separately, proving the Goal holds in each case.
  • (Formal system, Proof/Reason technique, Language feature/design, Programming paradigm) A proof technique in Rocq (via destruct or case) that splits a Goal into Subgoals for each constructor of an inductive type.