HOL.Conv
Description
data Result Source #
Constructors
Defined in HOL.Conv
Methods
(==) :: Result -> Result -> Bool #
(/=) :: Result -> Result -> Bool #
compare :: Result -> Result -> Ordering #
(<) :: Result -> Result -> Bool #
(<=) :: Result -> Result -> Bool #
(>) :: Result -> Result -> Bool #
(>=) :: Result -> Result -> Bool #
max :: Result -> Result -> Result #
min :: Result -> Result -> Result #
showsPrec :: Int -> Result -> ShowS #
show :: Result -> String #
showList :: [Result] -> ShowS #
newtype Conv Source #
apply :: Conv -> Term -> Maybe Result Source #
applyData :: Conv -> Conv -> Conv -> TermData -> Maybe Result Source #
applyTerm :: Conv -> Term -> Term Source #
fail :: Conv Source #
id :: Conv Source #
beta :: Conv Source #
betaSimp :: Conv Source #
orelse :: Conv -> Conv -> Conv Source #
thenc :: Conv -> Conv -> Conv Source #
try :: Conv -> Conv Source #
repeat :: Conv -> Conv Source #
sub :: Conv -> Conv Source #
rator :: Conv -> Conv Source #
rand :: Conv -> Conv Source #
abs :: Conv -> Conv Source #
cond :: (Term -> Bool) -> Conv -> Conv -> Conv Source #
bottomUp :: Conv -> Conv Source #
eval :: Conv -> Conv Source #