| Copyright | (c) Till Mossakowski, Uni Bremen 2002-2006 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | till@informatik.uni-bremen.de |
| Stability | provisional |
| Portability | non-portable(Logic) |
| Safe Haskell | Safe-Inferred |
CommonLogic.PredefinedCASLAxioms
Description
Fixed CASL axioms needed for translation of CommonLogic to CASL
- list :: Id
- append :: Id
- cons :: Id
- nil :: Id
- individual :: Id
- x1 :: Token
- x2 :: Token
- y1 :: Token
- y2 :: Token
- nilTypeS :: OpType
- consTypeS :: OpType
- appendTypeS :: OpType
- nilType :: OP_TYPE
- consType :: OP_TYPE
- appendType :: OP_TYPE
- baseListAxioms :: [Named CASLFORMULA]
- brId :: Id
- listSig :: CASLSign
- vx2 :: VAR_DECL
- vy1 :: VAR_DECL
- vy2 :: VAR_DECL
- tx1 :: TERM f
- ty2 :: TERM f
- ty1 :: TERM f
- tx2 :: TERM f
- consOp :: OP_SYMB
- nilOp :: OP_SYMB
- mkCons :: TERM f -> TERM f -> TERM f
- mkNil :: TERM f
- mkAppend :: TERM f -> TERM f -> TERM f
- ga_injective_cons :: Named CASLFORMULA
- ga_disjoint_nil_cons :: Named CASLFORMULA
- ga_nil_append :: Named CASLFORMULA
- ga_cons_append :: Named CASLFORMULA
- ga_generated_list :: Named CASLFORMULA
Documentation
individual :: Id