Safe Haskell	Safe-Inferred
Language	GHC2021

Logic.Proof

Contents

Proof Trees
Proof Generation
Proof Tree Manipulation

Synopsis

data Proof j = Node j [Proof j]
pattern Proof :: j -> [Proof j] -> Proof j
pattern Leaf :: j -> Proof j
class Explain j where
- premises :: j -> [[j]]
proofs :: Explain j => j -> [Proof j]
prove :: Explain j => j -> Maybe (Proof j)
prove' :: Explain j => j -> Proof j
suppose :: Explain j => j -> Proof j
conclusion :: Proof j -> j
children :: Proof j -> [Proof j]
hidePast :: Int -> Proof j -> Proof j
hide :: Eq j => j -> Proof j -> Maybe (Proof j)
countNodes :: Proof j -> Int
getRow :: Int -> Proof j -> [j]
toList :: Eq j => Proof j -> [j]
toList' :: Proof a -> [a]

Proof Trees

data Proof j #

The type of proof trees parameterized by the type of judgments j.

Constructors

Node j [Proof j]

Instances

Instances details

Foldable Proof #
Instance details Defined in Logic.Proof Methods fold :: Monoid m => Proof m -> m # foldMap :: Monoid m => (a -> m) -> Proof a -> m # foldMap' :: Monoid m => (a -> m) -> Proof a -> m # foldr :: (a -> b -> b) -> b -> Proof a -> b # foldr' :: (a -> b -> b) -> b -> Proof a -> b # foldl :: (b -> a -> b) -> b -> Proof a -> b # foldl' :: (b -> a -> b) -> b -> Proof a -> b # foldr1 :: (a -> a -> a) -> Proof a -> a # foldl1 :: (a -> a -> a) -> Proof a -> a # toList :: Proof a -> [a] # null :: Proof a -> Bool # length :: Proof a -> Int # elem :: Eq a => a -> Proof a -> Bool # maximum :: Ord a => Proof a -> a # minimum :: Ord a => Proof a -> a # sum :: Num a => Proof a -> a # product :: Num a => Proof a -> a #
Traversable Proof #
Instance details Defined in Logic.Proof Methods traverse :: Applicative f => (a -> f b) -> Proof a -> f (Proof b) # sequenceA :: Applicative f => Proof (f a) -> f (Proof a) # mapM :: Monad m => (a -> m b) -> Proof a -> m (Proof b) # sequence :: Monad m => Proof (m a) -> m (Proof a) #
Applicative Proof #
Instance details Defined in Logic.Proof Methods pure :: a -> Proof a # (<>) :: Proof (a -> b) -> Proof a -> Proof b # liftA2 :: (a -> b -> c) -> Proof a -> Proof b -> Proof c # (>) :: Proof a -> Proof b -> Proof b # (<*) :: Proof a -> Proof b -> Proof a #
Functor Proof #
Instance details Defined in Logic.Proof Methods fmap :: (a -> b) -> Proof a -> Proof b # (<$) :: a -> Proof b -> Proof a #
Monad Proof #
Instance details Defined in Logic.Proof Methods (>>=) :: Proof a -> (a -> Proof b) -> Proof b # (>>) :: Proof a -> Proof b -> Proof b # return :: a -> Proof a #
Show j => Show (Proof j) #
Instance details Defined in Logic.Proof Methods showsPrec :: Int -> Proof j -> ShowS # show :: Proof j -> String # showList :: [Proof j] -> ShowS #
Latex j => Latex (Proof j) #
Instance details Defined in Logic.Proof Methods latex :: Proof j -> String #

pattern Proof :: j -> [Proof j] -> Proof j #

A constructor synonym for Node.

pattern Leaf :: j -> Proof j #

A constructor synonym for Node with no premises.

Proof Generation

class Explain j where #

Methods

premises :: j -> [[j]] #

Returns a list of all possible premises of a given judgment.

premises j = [] if j is decidably false.A
premises j = [[]] if j is an axiom.
premises j = [p1,p2,...,pn] : tail (premises j) if j is provable from the conclusions of p1, p2, ..., pn.