hol-1.4: Higher order logic
Safe HaskellNone
LanguageHaskell2010

HOL.Conv

Description

 

Documentation

data Result Source #

Constructors

Unchanged 
Changed Thm 

Instances

Instances details
Eq Result Source # 
Instance details

Defined in HOL.Conv

Methods

(==) :: Result -> Result -> Bool #

(/=) :: Result -> Result -> Bool #

Ord Result Source # 
Instance details

Defined in HOL.Conv

Methods

compare :: Result -> Result -> Ordering #

(<) :: Result -> Result -> Bool #

(<=) :: Result -> Result -> Bool #

(>) :: Result -> Result -> Bool #

(>=) :: Result -> Result -> Bool #

max :: Result -> Result -> Result #

min :: Result -> Result -> Result #

Show Result Source # 
Instance details

Defined in HOL.Conv

Methods

showsPrec :: Int -> Result -> ShowS #

show :: Result -> String #

showList :: [Result] -> ShowS #

newtype Conv Source #

Constructors

Conv (Term -> Maybe Result) 

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 #