Data.Logic.ATP.PropExamples

Some propositional formulas to test, and functions to generate classes.

Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)

Documentation

data Knows a

Constructors

K String a (Maybe a)

Instances

Eq a => Eq (Knows a)

Ord a => Ord (Knows a)

Show a => Show (Knows a)

(Num a, Show a) => Pretty (Knows a)

Num a => HasFixity (Knows a)

IsAtom (Knows Integer)

mk_knows :: (IsPropositional formula, AtomOf formula ~ Knows a) => String -> a -> formula

mk_knows2 :: (IsPropositional formula, AtomOf formula ~ Knows a) => String -> a -> a -> formula

prime :: (IsPropositional formula, Ord formula, AtomOf formula ~ Knows Integer) => Integer -> formula

ramsey :: (IsPropositional pf, AtomOf pf ~ Knows Integer, Ord pf) => Integer -> Integer -> Integer -> pf

Generate assertion equivalent to R(s,t) <= n for the Ramsey number R(s,t)

testPropExamples :: Test