Merge branch 'master' of github.com:idris-lang/Idris-dev

docs/effects/state.rst

@@ -129,8 +129,8 @@ features, but for our purposes, it suffices to know the following:
 
 - ``x <- e`` binds the result of an effectful operation ``e`` to a
    variable ``x``. For example, in the above code, ``treeTagAux l`` is
-   an effectful operation returning a pair ``(Int, BTree a)``, so
-   ``l’`` has type ``(Int, BTree a)``.
+   an effectful operation returning ``BTree (Int, a)``, so ``l’`` has
+   type ``BTree (Int, a)``.
 
 - ``pure e`` turns a pure value ``e`` into the result of an effectful
    operation.

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

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