smtLib-1.0.8: A library for working with the SMTLIB format.

Safe HaskellSafe
LanguageHaskell98

SMTLib1

Synopsis

Documentation

newtype Name #

Constructors

N String 

Instances

Eq Name # 

Methods

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

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

Data Name # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Name -> c Name #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Name #

toConstr :: Name -> Constr #

dataTypeOf :: Name -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Name) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name) #

gmapT :: (forall b. Data b => b -> b) -> Name -> Name #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r #

gmapQ :: (forall d. Data d => d -> u) -> Name -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Name -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Name -> m Name #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name #

Ord Name # 

Methods

compare :: Name -> Name -> Ordering #

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

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

(>) :: Name -> Name -> Bool #

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

max :: Name -> Name -> Name #

min :: Name -> Name -> Name #

Show Name # 

Methods

showsPrec :: Int -> Name -> ShowS #

show :: Name -> String #

showList :: [Name] -> ShowS #

IsString Name # 

Methods

fromString :: String -> Name #

PP Name # 

Methods

pp :: Name -> Doc #

data Ident #

Constructors

I Name [Integer] 

Instances

Eq Ident # 

Methods

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

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

Data Ident # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Ident -> c Ident #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Ident #

toConstr :: Ident -> Constr #

dataTypeOf :: Ident -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Ident) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Ident) #

gmapT :: (forall b. Data b => b -> b) -> Ident -> Ident #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ident -> r #

gmapQ :: (forall d. Data d => d -> u) -> Ident -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Ident -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Ident -> m Ident #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Ident -> m Ident #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Ident -> m Ident #

Ord Ident # 

Methods

compare :: Ident -> Ident -> Ordering #

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

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

(>) :: Ident -> Ident -> Bool #

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

max :: Ident -> Ident -> Ident #

min :: Ident -> Ident -> Ident #

Show Ident # 

Methods

showsPrec :: Int -> Ident -> ShowS #

show :: Ident -> String #

showList :: [Ident] -> ShowS #

IsString Ident # 

Methods

fromString :: String -> Ident #

PP Ident # 

Methods

pp :: Ident -> Doc #

data Quant #

Constructors

Exists 
Forall 

Instances

Eq Quant # 

Methods

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

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

Data Quant # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Quant -> c Quant #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Quant #

toConstr :: Quant -> Constr #

dataTypeOf :: Quant -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Quant) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Quant) #

gmapT :: (forall b. Data b => b -> b) -> Quant -> Quant #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Quant -> r #

gmapQ :: (forall d. Data d => d -> u) -> Quant -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Quant -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Quant -> m Quant #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Quant -> m Quant #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Quant -> m Quant #

Ord Quant # 

Methods

compare :: Quant -> Quant -> Ordering #

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

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

(>) :: Quant -> Quant -> Bool #

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

max :: Quant -> Quant -> Quant #

min :: Quant -> Quant -> Quant #

Show Quant # 

Methods

showsPrec :: Int -> Quant -> ShowS #

show :: Quant -> String #

showList :: [Quant] -> ShowS #

PP Quant # 

Methods

pp :: Quant -> Doc #

data Conn #

Constructors

Not 
Implies 
And 
Or 
Xor 
Iff 
IfThenElse 

Instances

Eq Conn # 

Methods

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

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

Data Conn # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Conn -> c Conn #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Conn #

toConstr :: Conn -> Constr #

dataTypeOf :: Conn -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Conn) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Conn) #

gmapT :: (forall b. Data b => b -> b) -> Conn -> Conn #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Conn -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Conn -> r #

gmapQ :: (forall d. Data d => d -> u) -> Conn -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Conn -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Conn -> m Conn #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Conn -> m Conn #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Conn -> m Conn #

Ord Conn # 

Methods

compare :: Conn -> Conn -> Ordering #

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

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

(>) :: Conn -> Conn -> Bool #

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

max :: Conn -> Conn -> Conn #

min :: Conn -> Conn -> Conn #

Show Conn # 

Methods

showsPrec :: Int -> Conn -> ShowS #

show :: Conn -> String #

showList :: [Conn] -> ShowS #

PP Conn # 

Methods

pp :: Conn -> Doc #

data Formula #

Instances

Eq Formula # 

Methods

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

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

Data Formula # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Formula -> c Formula #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Formula #

toConstr :: Formula -> Constr #

dataTypeOf :: Formula -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Formula) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula) #

gmapT :: (forall b. Data b => b -> b) -> Formula -> Formula #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Formula -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Formula -> r #

gmapQ :: (forall d. Data d => d -> u) -> Formula -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Formula -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Formula -> m Formula #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Formula -> m Formula #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Formula -> m Formula #

Ord Formula # 
Show Formula # 
PP Formula # 

Methods

pp :: Formula -> Doc #

type Sort = Ident #

data Binder #

Constructors

Bind 

Fields

Instances

Eq Binder # 

Methods

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

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

Data Binder # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Binder -> c Binder #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Binder #

toConstr :: Binder -> Constr #

dataTypeOf :: Binder -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Binder) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Binder) #

gmapT :: (forall b. Data b => b -> b) -> Binder -> Binder #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Binder -> r #

gmapQ :: (forall d. Data d => d -> u) -> Binder -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Binder -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Binder -> m Binder #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder -> m Binder #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Binder -> m Binder #

Ord Binder # 
Show Binder # 
PP Binder # 

Methods

pp :: Binder -> Doc #

data Term #

Instances

Eq Term # 

Methods

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

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

Fractional Term # 

Methods

(/) :: Term -> Term -> Term #

recip :: Term -> Term #

fromRational :: Rational -> Term #

Data Term # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term -> c Term #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Term #

toConstr :: Term -> Constr #

dataTypeOf :: Term -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Term) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term) #

gmapT :: (forall b. Data b => b -> b) -> Term -> Term #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r #

gmapQ :: (forall d. Data d => d -> u) -> Term -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Term -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term -> m Term #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term #

Num Term # 

Methods

(+) :: Term -> Term -> Term #

(-) :: Term -> Term -> Term #

(*) :: Term -> Term -> Term #

negate :: Term -> Term #

abs :: Term -> Term #

signum :: Term -> Term #

fromInteger :: Integer -> Term #

Ord Term # 

Methods

compare :: Term -> Term -> Ordering #

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

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

(>) :: Term -> Term -> Bool #

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

max :: Term -> Term -> Term #

min :: Term -> Term -> Term #

Show Term # 

Methods

showsPrec :: Int -> Term -> ShowS #

show :: Term -> String #

showList :: [Term] -> ShowS #

IsString Term # 

Methods

fromString :: String -> Term #

PP Term # 

Methods

pp :: Term -> Doc #

data Literal #

Instances

Eq Literal # 

Methods

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

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

Data Literal # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Literal -> c Literal #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Literal #

toConstr :: Literal -> Constr #

dataTypeOf :: Literal -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Literal) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal) #

gmapT :: (forall b. Data b => b -> b) -> Literal -> Literal #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Literal -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Literal -> r #

gmapQ :: (forall d. Data d => d -> u) -> Literal -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Literal -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Literal -> m Literal #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Literal -> m Literal #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Literal -> m Literal #

Ord Literal # 
Show Literal # 
PP Literal # 

Methods

pp :: Literal -> Doc #

data Annot #

Constructors

Attr 

Instances

Eq Annot # 

Methods

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

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

Data Annot # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Annot -> c Annot #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Annot #

toConstr :: Annot -> Constr #

dataTypeOf :: Annot -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Annot) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Annot) #

gmapT :: (forall b. Data b => b -> b) -> Annot -> Annot #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annot -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annot -> r #

gmapQ :: (forall d. Data d => d -> u) -> Annot -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Annot -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Annot -> m Annot #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Annot -> m Annot #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Annot -> m Annot #

Ord Annot # 

Methods

compare :: Annot -> Annot -> Ordering #

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

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

(>) :: Annot -> Annot -> Bool #

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

max :: Annot -> Annot -> Annot #

min :: Annot -> Annot -> Annot #

Show Annot # 

Methods

showsPrec :: Int -> Annot -> ShowS #

show :: Annot -> String #

showList :: [Annot] -> ShowS #

PP Annot # 

Methods

pp :: Annot -> Doc #

data FunDecl #

Constructors

FunDecl 

Fields

Instances

Data FunDecl # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FunDecl -> c FunDecl #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FunDecl #

toConstr :: FunDecl -> Constr #

dataTypeOf :: FunDecl -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c FunDecl) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunDecl) #

gmapT :: (forall b. Data b => b -> b) -> FunDecl -> FunDecl #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunDecl -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunDecl -> r #

gmapQ :: (forall d. Data d => d -> u) -> FunDecl -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> FunDecl -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> FunDecl -> m FunDecl #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FunDecl -> m FunDecl #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FunDecl -> m FunDecl #

PP FunDecl # 

Methods

pp :: FunDecl -> Doc #

data PredDecl #

Constructors

PredDecl 

Fields

Instances

Data PredDecl # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PredDecl -> c PredDecl #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PredDecl #

toConstr :: PredDecl -> Constr #

dataTypeOf :: PredDecl -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c PredDecl) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PredDecl) #

gmapT :: (forall b. Data b => b -> b) -> PredDecl -> PredDecl #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PredDecl -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PredDecl -> r #

gmapQ :: (forall d. Data d => d -> u) -> PredDecl -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> PredDecl -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PredDecl -> m PredDecl #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PredDecl -> m PredDecl #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PredDecl -> m PredDecl #

PP PredDecl # 

Methods

pp :: PredDecl -> Doc #

data Status #

Constructors

Sat 
Unsat 
Unknown 

Instances

Data Status # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Status -> c Status #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Status #

toConstr :: Status -> Constr #

dataTypeOf :: Status -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Status) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Status) #

gmapT :: (forall b. Data b => b -> b) -> Status -> Status #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Status -> r #

gmapQ :: (forall d. Data d => d -> u) -> Status -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Status -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Status -> m Status #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Status -> m Status #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Status -> m Status #

PP Status # 

Methods

pp :: Status -> Doc #

data Command #

Instances

Data Command # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Command -> c Command #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Command #

toConstr :: Command -> Constr #

dataTypeOf :: Command -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Command) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Command) #

gmapT :: (forall b. Data b => b -> b) -> Command -> Command #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Command -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Command -> r #

gmapQ :: (forall d. Data d => d -> u) -> Command -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Command -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Command -> m Command #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Command -> m Command #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Command -> m Command #

PP Command # 

Methods

pp :: Command -> Doc #

data Script #

Constructors

Script 

Fields

Instances

PP Script # 

Methods

pp :: Script -> Doc #

(.<.) :: Term -> Term -> Formula #

For Int

(.>.) :: Term -> Term -> Formula #

For Int

funDef :: Ident -> [Sort] -> Sort -> Command #

class PP t where #

Minimal complete definition

pp

Methods

pp :: t -> Doc #

Instances

PP Script # 

Methods

pp :: Script -> Doc #

PP Command # 

Methods

pp :: Command -> Doc #

PP Status # 

Methods

pp :: Status -> Doc #

PP PredDecl # 

Methods

pp :: PredDecl -> Doc #

PP FunDecl # 

Methods

pp :: FunDecl -> Doc #

PP Annot # 

Methods

pp :: Annot -> Doc #

PP Literal # 

Methods

pp :: Literal -> Doc #

PP Term # 

Methods

pp :: Term -> Doc #

PP Binder # 

Methods

pp :: Binder -> Doc #

PP Formula # 

Methods

pp :: Formula -> Doc #

PP Conn # 

Methods

pp :: Conn -> Doc #

PP Quant # 

Methods

pp :: Quant -> Doc #

PP Ident # 

Methods

pp :: Ident -> Doc #

PP Name # 

Methods

pp :: Name -> Doc #