Copilot.Theorem

Documentation

instantiate :: Proof Universal -> Proof Existential

assume :: PropRef Universal -> Proof a

admit :: Proof a

type Proof a = ProofScheme a ()

type PropId = String

data PropRef a

data Universal

data Existential