Documentation

tipSign :: (CASLSign, [Named CASLFORMULA]) -> [Decl] Source #

fromOP_SYMBtoOpMapPair :: OP_SYMB -> (OP_NAME, OpType) Source #

tipAxiom :: Named CASLFORMULA -> Decl Source #

tipFORMULA :: CASLFORMULA -> Expr Source #

tipSOFORMULA :: Set (PRED_NAME, PredType) -> CASLFORMULA -> Expr Source #

tipSOTERM :: Set (PRED_NAME, PredType) -> TERM () -> Expr Source #

tipOP_SYMB :: OP_SYMB -> PolySymbol Source #

tipOP_NAME :: SORT -> [SORT] -> OP_NAME -> Symbol Source #

tipPRED_SYMB :: PRED_SYMB -> PolySymbol Source #

tipPRED_NAME :: [SORT] -> PRED_NAME -> Symbol Source #

tipProfile :: [SORT] -> Maybe SORT -> String Source #

tipRelation :: Relation -> Head Source #

tipJunctor :: Junctor -> Head Source #

tipQUANTIFIER :: QUANTIFIER -> Binder Source #

tipPredVAR_DECL :: PRED_NAME -> PredType -> [Binding] Source #

tipPredVAR :: [SORT] -> PRED_NAME -> Symbol Source #

tipVAR_DECL :: VAR_DECL -> [Binding] Source #

tipVAR :: SORT -> VAR -> Symbol Source #

tipSORT :: SORT -> Symbol Source #

qualNameToSymbol :: Show a => String -> Maybe SORT -> [SORT] -> a -> Symbol Source #

tipDatatype :: (SORT, [OP_SYMB]) -> (DatatypeName, Datatype) Source #

tipConstructor :: OP_SYMB -> Constructor Source #

tipSelector :: Symbol -> (SORT, Integer) -> Binding Source #

freeTypesAndCons :: [Named (FORMULA f)] -> [[(SORT, [OP_SYMB])]] Source #

declareSort :: SORT -> Decl Source #

declareOp :: (OP_NAME, OpType) -> Decl Source #

declarePred :: (PRED_NAME, PredType) -> Decl Source #