Data.Logic.ATP.Equate

ATOM with the Equate predicate

Documentation

class HasApply atom => HasEquate atom where

Atoms that support equality must have HasEquate instance

Methods

equate :: TermOf atom -> TermOf atom -> atom

foldEquate :: (TermOf atom -> TermOf atom -> r) -> (PredOf atom -> [TermOf atom] -> r) -> atom -> r

Instances

(IsPredicate predicate, IsTerm term) => HasEquate (FOL predicate term)

(.=.) :: (IsFormula formula, HasEquate atom, atom ~ AtomOf formula) => TermOf atom -> TermOf atom -> formula infix 6

Build an equality formula from two terms.

zipEquates :: HasEquate atom => (TermOf atom -> TermOf atom -> TermOf atom -> TermOf atom -> Maybe r) -> (PredOf atom -> [(TermOf atom, TermOf atom)] -> Maybe r) -> atom -> atom -> Maybe r

Zip two atoms that support equality

isEquate :: HasEquate atom => atom -> Bool

prettyEquate :: IsTerm term => PrettyLevel -> Rational -> term -> term -> Doc

Format the infix equality predicate applied to two terms.

overtermsEq :: HasEquate atom => (TermOf atom -> r -> r) -> r -> atom -> r

Implementation of overterms for HasApply types.

ontermsEq :: HasEquate atom => (TermOf atom -> TermOf atom) -> atom -> atom

Implementation of onterms for HasApply types.

showApplyAndEquate :: (HasEquate atom, Show (TermOf atom)) => atom -> String

Implementation of Show for HasEquate types

showEquate :: Show term => term -> term -> String

convertEquate :: (HasEquate atom1, HasEquate atom2) => (PredOf atom1 -> PredOf atom2) -> (TermOf atom1 -> TermOf atom2) -> atom1 -> atom2

precedenceEquate :: HasEquate atom => atom -> Precedence

associativityEquate :: HasEquate atom => atom -> Associativity

data FOL predicate term

Instance of an atom type with a distinct equality predicate.

Constructors

R predicate [term]

Equals term term

Instances

IsFirstOrder EqFormula

IsFirstOrder Formula

Unify SkAtom V SkTerm

(Eq predicate, Eq term) => Eq (FOL predicate term)

(Data predicate, Data term) => Data (FOL predicate term)

(Ord predicate, Ord term) => Ord (FOL predicate term)

(Read predicate, Read term) => Read (FOL predicate term)

(IsPredicate predicate, IsTerm term, Show predicate, Show term) => Show (FOL predicate term)

(HasApply (FOL predicate term), HasEquate (FOL predicate term), IsTerm term) => Pretty (FOL predicate term)

(IsPredicate predicate, IsTerm term) => HasFixity (FOL predicate term)

(IsPredicate predicate, IsTerm term) => IsAtom (FOL predicate term)

(IsPredicate predicate, IsTerm term) => HasApply (FOL predicate term)

(IsPredicate predicate, IsTerm term) => HasEquate (FOL predicate term)

type PredOf (FOL predicate term) = predicate

type TermOf (FOL predicate term) = term

type EqAtom = FOL Predicate FTerm

An atom type with equality predicate