f9f1885 · Idris-dev · git.iko.soy

contribs/lib/SimpleParser/SimpleParser.idr+15

@@ -150,6 +150,21 @@ symbol xs = token (string xs)

150strToken : Parser String

151strToken = map pack (token (many1 alphanum))

152

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

153

168

154--------------------------------------------------------------------------------

169--------------------------------------------------------------------------------

155-- Expressions

170-- 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):

360\begin{SaveVerbatim}{findecl}

361

362data Fin : Nat -> Type where

363− fO : Fin (S k)

363+ fZ : Fin (S k)

364 fS : Fin k -> Fin (S k)

365

366\end{SaveVerbatim}

367\useverb{findecl}

368

369\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;

371\texttt{fS n} is the

372\texttt{n+1}th element of a finite set with \texttt{S k} elements.

373\tTC{Fin} is indexed by a \tTC{Nat}, which