Documentation

preDefHCAssumps :: Set Id -> ConstMap

o1ci :: Constant -> ConstInfo

o2ci :: Constant -> ConstInfo

o3ci :: Constant -> ConstInfo

a2o1ci :: Constant -> ConstInfo

resci :: Constant -> ConstInfo

botci :: Constant -> ConstInfo

defci :: Constant -> ConstInfo

preDefAxioms :: Set Id -> [Named THFFormula]

mkNSD :: Constant -> (Constant -> String) -> Named THFFormula

genTHFFormula :: Constant -> (Constant -> String) -> THFFormula

notFS :: Constant -> String

falseFS :: Constant -> String

trueFS :: Constant -> String

andFS :: Constant -> String

orFS :: Constant -> String

eqvFS :: Constant -> String

implFS :: Constant -> String

ifFS :: Constant -> String

resFS :: Constant -> String

botFS :: Constant -> String

defFS :: Constant -> String

defnS :: String

encTHF :: String -> String