git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1991 from markfarrell/graph-and-polyhedra
84fa0bbDavid Christiansen
libs/contrib/Data/Graph.idrnew file+8
compare with master
unifiedsplit
@@ -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