|
|
|
|
| Synopsis |
|
|
|
| Documentation |
|
| data Signed a |
| Constructors | |  Instances | |
|
|
| sign :: Signed a -> Bool |
| The sign of a signed value
|
|
| flipSign :: Signed a -> Signed a |
| Flip a sign
|
|
| (+/-) :: Bool -> a -> Signed a |
|
| type HalfProof = Signed [ProofPart] |
Halve a proof,
A HalfProof for a could be for instance a|- ==> ... ==> goal
Two HalfProofs can be connected to form a full proof, with the root a |- a.
|
|
| data ProofPart |
| Constructors | | | Instances | |
|
|
| proofFalsum :: ProofPart -> Proof |
| Terminate a proof in false |- D.
|
|
| proofAssum :: Formula -> ProofPart -> ProofPart -> Proof |
| Terminate a proof in G, a |- a, D.
|
|
| proof1 :: ProofPart -> Proof -> Proof |
|
| data RProofStep0 |
|
|
| data RProofStep1 |
|
|
| data RProofStep2 |
|
|
| proofAnd :: Proof -> Proof -> Proof |
| Combine a |- b and c |- d into ...
|
|
| type Sign = Bool |
|
| data ProofStep0 |
|
|
| data ProofStep1 |
|
|
| data ProofStep2 |
|
|
| data ProofTree |
|
|
| type Sequent = Set (Signed Formula) |
|
| runProof :: ProofTree -> Sequent |
| Run a proof, return the resulting sequent
|
|
| joinProof :: ProofTree -> ProofTree -> ProofTree |
|
| data Proof |
| Constructors | | | Instances | |
|
|
| Produced by Haddock version 0.8 |
