Safe Haskell	Safe-Inferred
Language	Haskell2010

RSTT.Tope

Contents

Synopsis

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).

Instances details

IsString Tope Source #
Instance details Defined in RSTT.Tope Methods fromString :: String -> Tope #
Show Tope Source #
Instance details Defined in RSTT.Tope Methods showsPrec :: Int -> Tope -> ShowS # show :: Tope -> String # showList :: [Tope] -> ShowS #
Eq Tope Source #
Instance details Defined in RSTT.Tope Methods (==) :: Tope -> Tope -> Bool # (/=) :: Tope -> Tope -> Bool #
Ord Tope Source #
Instance details Defined in RSTT.Tope Methods compare :: Tope -> Tope -> Ordering # (<) :: Tope -> Tope -> Bool # (<=) :: Tope -> Tope -> Bool # (>) :: Tope -> Tope -> Bool # (>=) :: Tope -> Tope -> Bool # max :: Tope -> Tope -> Tope # min :: Tope -> Tope -> Tope #

A shape is a tope in a cube context (with just one cube point variable): $\{t : I \mid \phi \}$ .

Constructors

Shape
Fields shapePoint :: (Var, Cube) shapeTope :: Tope

Instances details

Show Shape Source #
Instance details Defined in RSTT.Tope Methods showsPrec :: Int -> Shape -> ShowS # show :: Shape -> String # showList :: [Shape] -> ShowS #
Eq Shape Source #
Instance details Defined in RSTT.Tope Methods (==) :: Shape -> Shape -> Bool # (/=) :: Shape -> Shape -> Bool #

A tope context consists of a set of topes.

Pretty-printing

Pretty-print a TopeContext.

Pretty-print a Shape.

Pretty-print a Tope.

Pretty-print a Tope expression in a given precedence environment.

Replace a point subterm everywhere in a tope term.

Replace a point subterm everywhere in a point term.

Check whether a point term is a subterm of another point term.