Expand description
Types for program extraction from constructive proofs (Curry-Howard correspondence).
Structs§
- Extracted
Program - A program extracted from a constructive proof via Curry-Howard.
- Program
Spec - A Hoare-style specification for a program.
Enums§
- Constructive
Prop - A constructive proposition in intuitionistic logic.
- Extraction
Result - Result of a program extraction attempt.
- Proof
Term - A proof term in the Curry-Howard correspondence. Each term witnesses a constructive proof of some proposition.