git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:edwinb/Idris-dev
commitf9f188551dab919b6e3f0ffc41c06f328182e411 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 2 Sep 2013, 16:00 (13 years ago) parent959e7b18be6b35
3 files changed+17−2
compare with master
unifiedsplit
contribs/lib/SimpleParser/SimpleParser.idr+15 tutorial/idris-tutorial.pdf tutorial/typesfuns.tex+2−2
contribs/lib/SimpleParser/SimpleParser.idr+15
@@ -150,6 +150,21 @@ symbol xs = token (string xs)
150150strToken : Parser String
151151strToken = map pack (token (many1 alphanum))
152152
153+--------------------------------------------------------------------------------
154+-- combinators
155+--------------------------------------------------------------------------------
156+
157+optional : Parser a -> Parser ()
158+optional p = (p $> pure ()) <|> pure ()
159+
160+sepBy1 : Parser a -> Parser b -> Parser (List a)
161+sepBy1 p s = [| p :: many (s $> p) |]
162+
163+sepBy : Parser a -> Parser b -> Parser (List a)
164+sepBy p s = sepBy1 p s <|> pure Nil
165+
166+manyTil : Parser a -> Parser b -> Parser (List a)
167+manyTil p e = (e $> pure Nil) <|> [| p :: manyTil p e |]
153168
154169--------------------------------------------------------------------------------
155170-- Expressions
tutorial/idris-tutorial.pdf

Binary file not shown.

tutorial/typesfuns.tex+2−2
@@ -360,14 +360,14 @@ They are declared as follows (again, in the prelude):
360360\begin{SaveVerbatim}{findecl}
361361
362362data Fin : Nat -> Type where
363− fO : Fin (S k)
363+ fZ : Fin (S k)
364364 fS : Fin k -> Fin (S k)
365365
366366\end{SaveVerbatim}
367367\useverb{findecl}
368368
369369\noindent
370−\tDC{fO} is the zeroth element of a finite set with \texttt{S k} elements;
370+\tDC{fZ} is the zeroth element of a finite set with \texttt{S k} elements;
371371\texttt{fS n} is the
372372\texttt{n+1}th element of a finite set with \texttt{S k} elements.
373373\tTC{Fin} is indexed by a \tTC{Nat}, which