Data.Graph & Data.Polyhedra
Signed-off-by: Mark Farrell <m4farrel@uwaterloo.ca>
commit45ef64928fa2f8be1dc5b203144cb3d78357a887
authorMark Farrell <m4farrel@uwaterloo.ca>
dateTue 10 Mar 2015, 17:50 (12 years ago)
parente9c96d4
libs/base/Data/Graph.idrnew file+8
@@ -0,0 +1,8 @@
1+module Data.Graph
2+
3+import Data.Vect
4+
5+data Edge e = MkEdge e e
6+
7+data Graph : Nat −> Nat −> Type −> Type −> Type where
8+ MkGraph : Vect m v −> Vect n (Edge k) −> Graph m n v k
libs/base/Data/Polyhedra.idrnew file+9
@@ -0,0 +1,9 @@
1+module Data.Polyhedra
2+
3+import Data.Vect
4+import Data.Graph
5+
6+data Face f = MkFace (Vect n f)
7+
8+data Polyhedron : Nat -> Nat -> Nat -> Type -> Type where
9+ MkPolyhedron : Vect k v -> Vect m (Edge v) -> Vect n (Face v) -> Polyhedron k m n v