Merge pull request #1991 from markfarrell/graph-and-polyhedra
Data.Graph & Data.Polyhedra
commit84fa0bbcaf3d2350df1d504a5bc864bb7a0cd32e
authorDavid Christiansen <david@davidchristiansen.dk>
dateSun 22 Mar 2015, 11:43 (12 years ago)
parente10c20557f1543
libs/contrib/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/contrib/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