Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- type Proof = ()
- toProof :: a -> Proof
- trivial :: Proof
- unreachable :: Proof
- (***) :: a -> QED -> Proof
- data QED
- (?) :: a -> b -> a
- (===) :: a -> a -> a
- (=<=) :: a -> a -> a
- (=>=) :: a -> a -> a
- (==.) :: a -> a -> a
- (==!) :: a -> a -> a
- (&&&) :: Proof -> Proof -> Proof
- withProof :: a -> b -> a
- impossible :: a -> b
Proof is just a () alias
Proof constructors
Proof Construction -------------------------------------------------------
trivial is proof by SMT
unreachable :: Proof Source #
(***) :: a -> QED -> Proof infixl 3 Source #
proof casting | `x *** QED`: x is a proof certificate* strong enough for SMT to prove your theorem | `x *** Admit`: x is an unfinished proof
Proof certificate constructors
These two operators check all intermediate equalities
(===) :: a -> a -> a infixl 3 Source #
- Checked Proof Certificates ---------------------------------------------
Implicit equality
This operator does not check intermediate equalities
(==.) :: a -> a -> a infixl 3 Source #
Deprecated: Use (===) instead
To summarize:
- (==!) is *only* for proof debugging - (===) does not require explicit proof term
- (?) lets you insert "lemmas" as other
Proof
values
- Unchecked Proof Certificates -------------------------------------------
The above operators check each intermediate proof step.
The operator ==.
below accepts an optional proof term
argument, but does not check intermediate steps.
TODO: What is it USEFUL FOR?
(==!) :: a -> a -> a infixl 3 Source #
Assumed equality `x ==! y ` returns the admitted proof certificate that result value is equals x and y
Combining Proofs
(&&&) :: Proof -> Proof -> Proof Source #
- Combining Proof Certificates -------------------------------------------
impossible :: a -> b Source #