4cfbff1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tinkered with syntax rules section in tutorial

commit4cfbff19d6633d36199ef4c94cea30f330f0f418 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 5 Jan 2012, 17:33 (15 years ago) parentf1ba88c

3 files changed+6−3

unifiedsplit

lib/builtins.idr+1

@@ -60,6 +60,7 @@ boolElim False t e = e;

6060data so : Bool -> Set where oh : so True;

6161

6262syntax if [test] then [t] else [e] = boolElim test t e;

63+syntax [test] "?" [t] ":" [e] = if test then t else e;

6364

6465infixl 4 &&, ||;

6566

tutorial/idris-tutorial.pdf

Binary file not shown.

tutorial/syntax.tex+5−3

@@ -38,15 +38,17 @@ and \texttt{[e]} here, which stand for arbitrary expressions

3838\end{itemize}

3939

4040\noindent

41−The only limitations on the form of a syntax rule are that it must include at least one

41+The limitations on the form of a syntax rule are that it must include at least one

4242symbol or keyword, and there must be no repeated variables standing for non-terminals.

43+Rules can use previously defined rules, but may not be recursive.

4344The following syntax extensions would therefore be valid:

4445

4546\begin{SaveVerbatim}{syntaxex}

4647

47−syntax [var] ":=" [val] = Assign var val

48−syntax select [x] from [t] = Select x t;

48+syntax [var] ":=" [val] = Assign var val;

49+syntax [test] "?" [t] ":" [e] = if test then t else e;

4950syntax select [x] from [t] where [w] = SelectWhere x t w;

51+syntax select [x] from [t] = Select x t;

5052

5153\end{SaveVerbatim}

5254\useverb{syntaxex}