Copyright | (c) Isaac van Bakel 2020 |
---|---|

License | BSD-3 |

Maintainer | ivb@vanbakel.io |

Stability | experimental |

Portability | POSIX |

Safe Haskell | Safe |

Language | Haskell2010 |

This module contains some helpers for declaring proofs, and running them as code.

# Documentation

runProof :: Theorem a -> a Source #

Run a theorem to its Haskell term. If the proof of the theorem uses only terminating values, then the resulting Haskell term can be run as usual without errors.

A proven theorem.

As described in Hout.Prover.Tactics, proof of `a`

is equivalent to reducing
the proof goal `a`

to the trival proof goal `()`

.

type Definition a = Theorem a Source #

Admit an axiom, without proof. Note that this is not a terminating term, so using it will not yield computable Haskell.

noncomputable :: Axiom a -> a Source #

Use an axiom, with the understood caveat that the result will not be a
computable term. It is impossible to construct an `Axiom`

, so using one
cannot give runnable Haskell.