@@ -92,6 +92,27 @@ of these patterns.
9292We will return to this function in Section :ref:`sect-provisional` to
9393complete the definition of ``parity``.
9494
95+With and proofs
96+===============
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:
101+
102+.. code-block:: idris
103+
104+ data Foo = FInt Int | FBool Bool
105+
106+ optional : Foo -> Maybe Int
107+ optional (FInt x) = Just x
108+ optional (FBool b) = Nothing
109+
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
114+
115+
95116.. [1] Conor McBride and James McKinna. 2004. The view from the
96117 left. J. Funct. Program. 14, 1 (January 2004),
97118 69-111. DOI=10.1017/S0956796803004829