scrambled
scrambled
Concept

Proof

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

Tools: Rocq (formerly Coq)

  • (Logic, Proof/Reason technique) A logical argument establishing the truth of a proposition.
  • (Language feature/design, Programming paradigm, Formal system, Proof/Reason technique) In Rocq, a term of a propositional type constructed interactively via tactics or directly as a term. This draws from the Curry-Howard correspondence.