Expand description
Theorem and proof block AST types.
This module defines the AST for theorem blocks in the vernacular proof language:
## Theorem: Socrates_Mortality
Given: All men are mortal.
Given: Socrates is a man.
Prove: Socrates is mortal.
Proof: Auto.§Key Types
TheoremBlock: Contains premises, goal, and proof strategyProofStrategy: How to prove (Auto, Manual, By lemmas)
Structs§
- Theorem
Block - A theorem block containing premises, goal, and proof strategy.
Enums§
- Proof
Strategy - Proof strategies for theorem verification.