content: {- |
  Module      :  ./CASL/OMDoc.hs
  Description :  CASL specific OMDoc constants
  Copyright   :  (c) Ewaryst Schulz, DFKI Bremen 2009
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  ewaryst.schulz@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  Library of CASL specific OMDoc constants
  -}
  
  module CASL.OMDoc where
  
  import OMDoc.DataTypes
  
  -- * Meta theory
  
  -- | CASL meta theory content dictionary
  caslMetaTheory :: OMCD
  caslMetaTheory = CD ["casl", "http://cds.omdoc.org/logics/casl/casl.omdoc"]
  
  
  -- * Terms
  
  -- cdbase entries missing for predefined content dictionaries
  
  const_casl :: String -> OMElement
  const_casl n = OMS (caslMetaTheory, mkSimpleName n)
  
  const_true, const_false, const_sort, const_funtype, const_partialfuntype
   , const_and, const_or, const_implies, const_implied, const_equivalent
   , const_forall, const_exists, const_eq, const_eeq, const_existsunique
   , const_def, const_in, const_if, const_cast, const_type, const_not
   , const_predtype, const_subsortof :: OMElement
  
  const_true = const_casl "true"
  const_false = const_casl "false"
  
  const_funtype = const_casl "funtype"
  const_partialfuntype = const_casl "partialfuntype"
  const_predtype = const_casl "predtype"
  const_type = const_casl "type"
  const_subsortof = const_casl "subsortof"
  
  const_not = const_casl "not"
  const_and = const_casl "and"
  const_or = const_casl "or"
  const_implies = const_casl "implies"
  const_implied = const_casl "implied"
  const_equivalent = const_casl "equivalent"
  
  const_forall = const_casl "forall"
  const_exists = const_casl "exists"
  
  const_eq = const_casl "eq"
  const_eeq = const_casl "eeq"
  const_existsunique = const_casl "existsunique"
  const_def = const_casl "def"
  const_in = const_casl "in"
  const_if = const_casl "if"
  const_cast = const_casl "cast"
  const_sort = const_casl "sort"
  