| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
RSTT.Cube
Contents
Documentation
A label (constructor symbol).
A variable.
A cube expression.
Constructors
| CubeUnit | Unit cube: \(\mathbb{1}\). |
| CubeProduct Cube Cube | Product of cubes: \(I \times J\). |
| CubeCon Label | A user-defined cube, e.g. \(\mathbb{2}, \mathbb{I}\). |
| CubeVar Var | A cube variable: \(I, J\). |
A point in a cube.
Constructors
| PointUnit | The only point in the unit cube: \(\star : \mathbb{1}\). |
| PointPair Point Point | A pair of points: \(t : I, s : J \vdash \langle t, s \rangle : I \times J\). |
| PointFirst Point | First projection: \(\pi_1\;t\). |
| PointSecond Point | Second projection: \(\pi_2\;t\). |
| PointCon Label [Point] | A user-defined point constructor, e.g. \(0 : \mathbb{2}\) or \(t \land s : \mathbb{I}\). |
| PointVar Var | A point variable: \(t, s\). |
type CubeContext = [(Var, Cube)] Source #
A cube context consists of point variables with corresponding cubes.
Pretty-printing
ppCubeContext :: CubeContext -> String Source #
Pretty-print a CubeContext.