Copyright | (c) University of Cambridge, Cambridge, England adaption (c) Till Mossakowski, Uni Bremen 2002-2005 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | Christian.Maeder@dfki.de |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
translate Id
to Isabelle strings
- showIsaConstT :: Id -> BaseSig -> String
- showIsaConstIT :: Id -> Int -> BaseSig -> String
- showIsaTypeT :: Id -> BaseSig -> String
- transConstStringT :: BaseSig -> String -> String
- transTypeStringT :: BaseSig -> String -> String
- mkIsaConstT :: Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set String -> VName
- mkIsaConstIT :: Bool -> GlobalAnnos -> Int -> Id -> Int -> BaseSig -> Set String -> VName
- transString :: String -> String
- isaPrelude :: IsaPreludes
- data IsaPreludes = IsaPreludes {}
- getConstIsaToks :: Id -> Int -> BaseSig -> Set String
Documentation
showIsaConstT :: Id -> BaseSig -> String
showIsaConstIT :: Id -> Int -> BaseSig -> String
add a number for overloading
showIsaTypeT :: Id -> BaseSig -> String
transConstStringT :: BaseSig -> String -> String
transTypeStringT :: BaseSig -> String -> String
mkIsaConstT :: Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set String -> VName
mkIsaConstIT :: Bool -> GlobalAnnos -> Int -> Id -> Int -> BaseSig -> Set String -> VName
transString :: String -> String
translate to a valid Isabelle string possibly non-injectively
data IsaPreludes