| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
HOL.OpenTheory.Interpret
Description
Synopsis
- data Symbol
- symbolName :: Symbol -> Name
- renameSymbol :: Symbol -> Name -> Symbol
- data Rename = Rename Symbol Name
- destRename :: Rename -> (Symbol, Name)
- newtype Renames = Renames {
- destRenames :: [Rename]
- concatRenames :: [Renames] -> Renames
- data Interpret = Interpret (Map Symbol Name)
- mk :: Map Symbol Name -> Interpret
- empty :: Interpret
- toRenames :: Interpret -> Renames
- fromRenames :: Renames -> Maybe Interpret
- fromRenamesUnsafe :: Renames -> Interpret
- interpret :: Interpret -> Symbol -> Name
- interpretTypeOp :: Interpret -> Name -> Name
- interpretConst :: Interpret -> Name -> Name
- compose :: Interpret -> Interpret -> Interpret
Documentation
Constructors
| TypeOpSymbol Name | |
| ConstSymbol Name |
symbolName :: Symbol -> Name Source #
Constructors
| Renames | |
Fields
| |
concatRenames :: [Renames] -> Renames Source #
fromRenamesUnsafe :: Renames -> Interpret Source #