@@ -92,6 +92,13 @@ of these patterns.
92We will return to this function in Section :ref:`sect-provisional` to
92We will return to this function in Section :ref:`sect-provisional` to
93complete the definition of ``parity``.
93complete the definition of ``parity``.
97+To use a dependent pattern match for theorem proving, it is sometimes necessary
98+to explicitly retain and name the proof generated by the pattern match.
99+To do this, you can postfix the with clause with ``proof p`` and the proof
100+generated by the pattern match will be in scope and named ``p``.
95.. [1] Conor McBride and James McKinna. 2004. The view from the
102.. [1] Conor McBride and James McKinna. 2004. The view from the
96 left. J. Funct. Program. 14, 1 (January 2004),
103 left. J. Funct. Program. 14, 1 (January 2004),
97 69-111. DOI=10.1017/S0956796803004829
104 69-111. DOI=10.1017/S0956796803004829