HOL.Conv

Documentation

data Result

Constructors

Unchanged

Changed Thm

Instances

Eq Result

Methods

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

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

Ord Result

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

Methods

showsPrec :: Int -> Result -> ShowS

show :: Result -> String

showList :: [Result] -> ShowS

newtype Conv

Constructors

Conv (Term -> Maybe Result)

apply :: Conv -> Term -> Maybe Result

applyData :: Conv -> TermData -> Maybe Result

applyTerm :: Conv -> Term -> Term

fail :: Conv

id :: Conv

beta :: Conv

orelse :: Conv -> Conv -> Conv

thenc :: Conv -> Conv -> Conv

try :: Conv -> Conv

repeat :: Conv -> Conv

sub :: Conv -> Conv

bottomUp :: Conv -> Conv