Concept

Goal

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

Tools: Rocq (formerly Coq)

  • (Formal system, Proof/Reason technique, Language feature/design, Programming paradigm) In Rocq, the Proposition to be proven at any point during a proof, which Tactics transform until it becomes trivially true.
  • (Formal system, Proof/Reason technique, Logic) A Proposition to be proven.