Codec.TPTP.Base

Basic undecorated formulae and terms

type Formula

type Term

Formulae and terms decorated with state

type FormulaST s

type TermST s

type FormulaC

type TermC

forgetFC

forgetTC

(.<=>.)

(.=>.)

(.<=.)

(.|.)

(.&.)

(.<~>.)

(.~|.)

(.~&.)

(.~.)

(.=.)

(.!=.)

for_all

exists

pApp

var

fApp

numberLitTerm

distinctObjectTerm

General decorated formulae and terms

data Formula0 term formula

data Term0 term

data BinOp

data InfixPred

data Quant

Formula Metadata

type TPTP_Input

type TPTP_Input_C

forgetTIC

data TPTP_Input_ c

data Annotations

data UsefulInfo

data Role

data GData

data GTerm

Gathering free Variables

class FreeVars a

univquant_free_vars

data AtomicWord

data V

Fixed-point style decorated formulae and terms

data F c

data T c

Utility functions

unwrapF

unwrapT

foldFormula0

foldTerm0

foldF

foldT