on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
commit9afcb72491b72da134004bc2ac0a663abdb73d53 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 22 Mar 2015, 13:20 (12 years ago) parent1bd70a1efda0d0
3 files changed+19−2
docs/effects/state.rst+2−2 libs/contrib/Data/Graph.idr+8 libs/contrib/Data/Polyhedra.idr+9
docs/effects/state.rst+2−2
@@ -129,8 +129,8 @@ features, but for our purposes, it suffices to know the following:
129129
130130- ``x <- e`` binds the result of an effectful operation ``e`` to a
131131 variable ``x``. For example, in the above code, ``treeTagAux l`` is
132− an effectful operation returning a pair ``(Int, BTree a)``, so
133− ``l’`` has type ``(Int, BTree a)``.
132+ an effectful operation returning ``BTree (Int, a)``, so ``l’`` has
133+ type ``BTree (Int, a)``.
134134
135135- ``pure e`` turns a pure value ``e`` into the result of an effectful
136136 operation.
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