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

lib/builtins.idr+1

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

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

61

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

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

63

64

64infixl 4 &&, ||;

65infixl 4 &&, ||;

65

66

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

38\end{itemize}

39

40\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

42symbol 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.

43The following syntax extensions would therefore be valid:

44The following syntax extensions would therefore be valid:

44

45

45\begin{SaveVerbatim}{syntaxex}

46\begin{SaveVerbatim}{syntaxex}

46

47

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

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

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

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

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

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

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

50

52

51\end{SaveVerbatim}

53\end{SaveVerbatim}

52\useverb{syntaxex}

54\useverb{syntaxex}