@@ -55,3 +55,35 @@ syntax select [x] from [t] = Select x t;
5555\end{SaveVerbatim}
5656\useverb{syntaxex}
5757
58+\noindent
59+Syntax macros can be further restricted to apply only in patterns (i.e., only on the left
60+hand side of a pattern match clause) or only in terms (i.e. everywhere but the left hand side
61+of a pattern match clause) by being marked as \texttt{pattern} or \texttt{term} syntax
62+rules. For example, we might define an interval as follows, with a static check
63+that the lower bound is below the upper bound using \texttt{so}:
64+
65+\begin{SaveVerbatim}{interval}
66+
67+data Interval : Set where
68+ MkInterval : (lower : Float) -> (upper : Float) ->
69+ so (lower < upper) -> Interval
70+
71+\end{SaveVerbatim}
72+\useverb{interval}
73+
74+\noindent
75+We can define a syntax which, in patterns, always matches \texttt{oh} for the proof
76+argument, and in terms requires a proof term to be provided:
77+
78+\begin{SaveVerbatim}{intervalsyn}
79+
80+pattern syntax "[" [x] "..." [y] "]" = MkInterval x y oh
81+term syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
82+
83+\end{SaveVerbatim}
84+\useverb{intervalsyn}
85+
86+\noindent
87+In terms, the syntax \texttt{[x...y]} will generate a proof obligation
88+\texttt{bounds\_lemma} (possibly renamed).
89+