@@ -92,6 +92,27 @@ 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 construct the proof resulting from 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``. For example:
102+.. code-block:: idris
104+ data Foo = FInt Int | FBool Bool
106+ optional : Foo -> Maybe Int
107+ optional (FInt x) = Just x
108+ optional (FBool b) = Nothing
110+ isFInt : (foo:Foo) -> Maybe (x : Int ** (optional foo = Just x))
111+ isFInt foo with (optional foo) proof p
112+ isFInt foo | Nothing = Nothing -- here, p : Nothing = optional foo
113+ isFInt foo | (Just x) = Just (x ** Refl) -- here, p : Just x = optional foo
95.. [1] Conor McBride and James McKinna. 2004. The view from the
116.. [1] Conor McBride and James McKinna. 2004. The view from the
96 left. J. Funct. Program. 14, 1 (January 2004),
117 left. J. Funct. Program. 14, 1 (January 2004),
97 69-111. DOI=10.1017/S0956796803004829
118 69-111. DOI=10.1017/S0956796803004829