| 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 |
Isabelle.Translate
Description
translate Id to Isabelle strings
Synopsis
- 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 Source #
showIsaConstIT :: Id -> Int -> BaseSig -> String Source #
add a number for overloading
showIsaTypeT :: Id -> BaseSig -> String Source #
transConstStringT :: BaseSig -> String -> String Source #
transTypeStringT :: BaseSig -> String -> String Source #
mkIsaConstT :: Bool -> GlobalAnnos -> Int -> Id -> BaseSig -> Set String -> VName Source #
mkIsaConstIT :: Bool -> GlobalAnnos -> Int -> Id -> Int -> BaseSig -> Set String -> VName Source #
transString :: String -> String Source #
translate to a valid Isabelle string possibly non-injectively
data IsaPreludes Source #
Constructors
| IsaPreludes | |
getConstIsaToks :: Id -> Int -> BaseSig -> Set String Source #
get the tokens of the alternative syntax that should not be used as variables