Merge pull request #1991 from markfarrell/graph-and-polyhedra

Data.Graph & Data.Polyhedra
idris-lang · Mar 22, 2015 · 84fa0bb · 84fa0bb
2 parents e10c205 + 57f1543
commit 84fa0bb
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 0 deletions.
diff --git a/libs/contrib/Data/Graph.idr b/libs/contrib/Data/Graph.idr
@@ -0,0 +1,8 @@
+module Data.Graph
+
+import Data.Vect
+
+data Edge e = MkEdge e e
+
+data Graph : Nat −> Nat −> Type −> Type −> Type where
+  MkGraph : Vect m v −> Vect n (Edge k) −> Graph m n v k
diff --git a/libs/contrib/Data/Polyhedra.idr b/libs/contrib/Data/Polyhedra.idr
@@ -0,0 +1,9 @@
+module Data.Polyhedra
+
+import Data.Vect
+import Data.Graph
+
+data Face f = MkFace (Vect n f)
+
+data Polyhedron : Nat -> Nat -> Nat -> Type -> Type where
+  MkPolyhedron : Vect k v -> Vect m (Edge v) -> Vect n (Face v) -> Polyhedron k m n v