Proof.QED.Advanced

Documentation

data Known

All these things are append only

Constructors

Known

Fields

definitions :: [(Var, Exp)]

types :: [(String, [(Con, Int)])]

assumed :: [Prop]

proved :: [Prop]

cheater :: Bool

Instances

Show Known

NFData Known

getKnown :: QED Known

data Unknown

Constructors

Unknown

Fields

goals :: [Goal]

focusSide :: Maybe Side

focusAt :: Int

Instances

Show Unknown

NFData Unknown

getUnknown :: Proof (Known, Unknown)

data Goal

Constructors

Goal [Prop] Prop

Instances

Show Goal

NFData Goal

getGoal :: Proof (Known, Unknown, Goal)

newtype BadProof

Constructors

BadProof String

Instances

Show BadProof

Exception BadProof

badProof :: String -> Proof a

isBadProof :: Proof () -> Proof Bool

newtype Laws

Constructors

Laws [Prop]

Instances

Monoid Laws

rewriteUnfold :: Prop -> Proof ()

Use a new prop which is the same as the previous goal, but with any number of unfoldings

rewriteEquivalent :: Prop -> Proof ()

Use a new prop which is the same as the first goals prop, but with simplified/rearranged expressions

rewriteRecurse :: Proof ()

Apply the coinduction principle on the computation

rewriteSplit :: Proof ()

Split the expression into multiple subexpressions

rewriteTautology :: Proof ()

The first goal is a tautology