acl2-0.0.1: Writing and calling ACL2 from Haskell.

Safe Haskell	Safe-Inferred
Language	Haskell98

Language.ACL2

Description

A DSL for ACL2.

Documentation

data Expr Source

Constructors

Obj [Expr]
Lit String

Instances

Eq Expr
Num Expr
Ord Expr
Show Expr

check :: [Expr] -> IO Bool Source

check' :: [Expr] -> IO (Bool, String) Source

mutualRecursion :: [Expr] -> Expr Source

defun :: String -> [String] -> Expr -> Expr Source

defun' :: String -> [String] -> Expr -> Expr -> Expr Source

defconst :: String -> Expr -> Expr Source

defthm :: String -> Expr -> Expr Source

thm :: Expr -> Expr Source

call :: String -> [Expr] -> Expr Source

obj :: [Expr] -> Expr Source

quote :: Expr -> Expr Source

consp :: Expr -> Expr Source

cons :: Expr -> Expr -> Expr Source

car :: Expr -> Expr Source

cdr :: Expr -> Expr Source

nth :: Expr -> Expr -> Expr Source

len :: Expr -> Expr Source

take' :: Expr -> Expr -> Expr Source

nthcdr :: Expr -> Expr -> Expr Source

updateNth :: Expr -> Expr -> Expr -> Expr Source

append :: Expr -> Expr -> Expr Source

let' :: [(String, Expr)] -> Expr -> Expr Source

if' :: Expr -> Expr -> Expr -> Expr Source

case' :: Expr -> [(Expr, Expr)] -> Expr -> Expr Source

assoc :: Expr -> Expr -> Expr Source

var :: String -> Expr Source

list :: [Expr] -> Expr Source

lit :: String -> Expr Source

string :: String -> Expr Source

nil :: Expr Source

t :: Expr Source

zp :: Expr -> Expr Source

zip' :: Expr -> Expr Source

undefined' :: Expr Source

equal :: Expr -> Expr -> Expr Source

not' :: Expr -> Expr Source

and' :: Expr -> Expr -> Expr Source

or' :: Expr -> Expr -> Expr Source

implies :: Expr -> Expr -> Expr Source

goodbye :: Expr Source

integerp :: Expr -> Expr Source

mod' :: Expr -> Expr -> Expr Source

(<.) :: Expr -> Expr -> Expr Source

(>.) :: Expr -> Expr -> Expr Source

(<=.) :: Expr -> Expr -> Expr Source

(>=.) :: Expr -> Expr -> Expr Source