{-# LANGUAGE GADTs #-}
module Proof where
-- Prop is a synonym for String, and represents
-- logical propositions. Note that 'type'
-- introduces a type synonym, i.e. Prop and String
-- can now be used completely interchangeably.
type Prop = String
-- An inference rule is a list of premises and a conclusion.
data Rule where
R :: [Prop] -> Prop -> Rule
deriving Show
-- A rule system is a list of rules.
type System = [Rule]
-- A proof is a tree where each node contains a rule and
-- a list of proofs of the rule's premises.
data Proof where
PNode :: Rule -> [Proof] -> Proof
deriving Show