ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-15 01:25:05 +03:00
Code Issues Projects Releases Wiki Activity

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

Browse Source 
Data.Graph & Data.Polyhedra
This commit is contained in:
David Christiansen 2015-03-22 11:43:14 +01:00
commit 84fa0bbcaf
2 changed files with 17 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libs/contrib/Data/Graph.idr Normal file
View File

@ -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

9
libs/contrib/Data/Polyhedra.idr Normal file
View File

@ -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