| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
RSTT.Tope
Contents
Synopsis
- data Tope
- data Shape = Shape {
- shapePoint :: (Var, Cube)
- shapeTope :: Tope
- type TopeContext = [Tope]
- ppTopeContext :: TopeContext -> String
- ppShape :: Shape -> String
- ppTope :: Tope -> String
- ppTopePrec :: Int -> Tope -> String
- replacePointInTope :: Point -> Point -> Tope -> Tope
- replacePoint :: Point -> Point -> Point -> Point
- subPointOf :: Point -> Point -> Bool
Documentation
A tope expression.
Constructors
| TopeTop | Top tope: \(\top\). |
| TopeBottom | Bottom tope: \(\bot\). |
| TopeAnd Tope Tope | AND tope: \(\phi \land \psi\). |
| TopeOr Tope Tope | OR tope: \(\phi \lor \psi\). |
| TopeEQ Point Point | Point equality tope: \(t \equiv s\). |
| TopeVar Var | A tope variable. |
| TopeImplies Tope Tope | IMPLIES tope: \(\phi \Rightarrow \psi\). NOTE: this tope is added to internalise known tope judgements and simplify proof search. |
| TopeCon Label [Point] | User-defined tope constructor (fully applied to some points). |
A shape is a tope in a cube context (with just one cube point variable): \(\{t : I \mid \phi \}\).
type TopeContext = [Tope] Source #
A tope context consists of a set of topes.
Pretty-printing
ppTopeContext :: TopeContext -> String Source #
Pretty-print a TopeContext.
ppTopePrec :: Int -> Tope -> String Source #
Pretty-print a Tope expression in a given precedence environment.
replacePointInTope :: Point -> Point -> Tope -> Tope Source #
Replace a point subterm everywhere in a tope term.