logic-classes-1.4.8: Framework for propositional and first order logic, theorem proving

Safe HaskellNone



class (Ord term, Variable v, Function f v) => Term term v f | term -> v f whereSource


vt :: v -> termSource

Build a term which is a variable reference.

fApp :: f -> [term] -> termSource

Build a term by applying terms to an atomic function. f (atomic function) is one of the type parameters, this package is mostly indifferent to its internal structure.

foldTerm :: (v -> r) -> (f -> [term] -> r) -> term -> rSource

A fold for the term data type, which understands terms built from a variable and a term built from the application of a primitive function to other terms.

zipTerms :: (v -> v -> Maybe r) -> (f -> [term] -> f -> [term] -> Maybe r) -> term -> term -> Maybe rSource


Term TermType String Function 
(Variable v, Function f v) => Term (NormalTerm v f) v f 
(Variable v, Function f v) => Term (CTerm v f) v f 
(Variable v, Function f v) => Term (PTerm v f) v f 

class (Eq f, Ord f, Skolem f v, Data f, Pretty f) => Function f v Source

convertTerm :: forall term1 v1 f1 term2 v2 f2. (Term term1 v1 f1, Term term2 v2 f2) => (v1 -> v2) -> (f1 -> f2) -> term1 -> term2Source

showTerm :: forall term v f. (Term term v f, Show v, Show f) => term -> StringSource

prettyTerm :: forall v f term. Term term v f => (v -> Doc) -> (f -> Doc) -> term -> DocSource

fvt :: (Term term v f, Ord v) => term -> Set vSource

tsubst :: (Term term v f, Ord v) => Map v term -> term -> termSource

funcs :: (Term term v f, Ord f) => term -> Set (f, Int)Source