Safe Haskell	None
Language	Haskell98

Proof.QED.Internal

Synopsis

Documentation

data Exp Source

Constructors

Var Var
Con Con
App Exp Exp
Let Var Exp Exp
Lam Var Exp
Case Exp [(Pat, Exp)]

Instances

Eq Exp Source
Data Exp Source
Ord Exp Source
Read Exp Source
Show Exp Source
NFData Exp Source

data Pat Source

Constructors

PCon Con [Var]
PWild

Instances

Eq Pat Source
Data Pat Source
Ord Pat Source
NFData Pat Source

newtype Var Source

Constructors

V
Fields fromVar :: String

Instances

Eq Var Source
Data Var Source
Ord Var Source
Show Var Source
NFData Var Source

newtype Con Source

Constructors

C
Fields fromCon :: String

Instances

Eq Con Source
Data Con Source
Ord Con Source
Show Con Source
NFData Con Source

data Prop Source

Constructors

Prop [Var] Exp Exp

Instances

Eq Prop Source
Data Prop Source
Read Prop Source
Show Prop Source
NFData Prop Source

data Side Source

Constructors

LHS
RHS

Instances

Eq Side Source
Show Side Source
NFData Side Source

data Known Source

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 Source
NFData Known Source

getKnown :: QED Known Source

data Unknown Source

Constructors

Unknown
Fields goals :: [Goal] focusSide :: Maybe Side focusAt :: Int

Instances

Show Unknown Source
NFData Unknown Source

getUnknown :: Proof (Known, Unknown) Source

data Goal Source

Constructors

Goal [Prop] Prop

Instances

Show Goal Source
NFData Goal Source

getGoal :: Proof (Known, Unknown, Goal) Source

newtype BadProof Source

Constructors

BadProof String

Instances

Show BadProof Source
Exception BadProof Source

badProof :: String -> Proof a Source

isBadProof :: Proof () -> Proof Bool Source

newtype Laws Source

Constructors

Laws [Prop]

Instances

Monoid Laws Source

rewriteUnfold :: Prop -> Proof () Source

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

rewriteEquivalent :: Prop -> Proof () Source

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

rewriteRecurse :: Proof () Source

Apply the coinduction principle on the computation

rewriteSplit :: Proof () Source

Split the expression into multiple subexpressions

rewriteTautology :: Proof () Source

The first goal is a tautology