| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Data.Logic.ATP.Equal
Contents
Description
First order logic with equality.
Copyright (co) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)
- function_congruence :: forall fof atom term v p function. (atom ~ AtomOf fof, term ~ TermOf atom, p ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, IsQuantified fof, HasEquate atom, IsTerm term, Ord fof) => (function, Int) -> Set fof
- equalitize :: forall formula atom term v function. (atom ~ AtomOf formula, term ~ TermOf atom, v ~ VarOf formula, v ~ TVarOf term, function ~ FunOf term, IsQuantified formula, HasEquate atom, IsTerm term, Ord formula, Ord atom) => formula -> formula
- wishnu :: Formula
- testEqual :: Test
Documentation
function_congruence :: forall fof atom term v p function. (atom ~ AtomOf fof, term ~ TermOf atom, p ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, IsQuantified fof, HasEquate atom, IsTerm term, Ord fof) => (function, Int) -> Set fof Source #
Code to generate equate axioms for functions.
equalitize :: forall formula atom term v function. (atom ~ AtomOf formula, term ~ TermOf atom, v ~ VarOf formula, v ~ TVarOf term, function ~ FunOf term, IsQuantified formula, HasEquate atom, IsTerm term, Ord formula, Ord atom) => formula -> formula Source #