@@ -71,6 +71,15 @@ Provisional definitions are written in the same way as ordinary
7171definitions, except that they introduce the right hand side with a
7272``?=`` rather than ``=``. We define ``parity`` as follows:
7373
74+.. code-block:: idris
75+
76+ parity : (n:Nat) -> Parity n
77+ parity Z = Even {n=Z}
78+ parity (S Z) = Odd {n=Z}
79+ parity (S (S k)) with (parity k)
80+ parity (S (S (j + j))) | Even ?= Even {n=S j}
81+ parity (S (S (S (j + j)))) | Odd ?= Odd {n=S j}
82+
7483When written in this form, instead of reporting a type error, Idris
7584will insert a metavariable standing for a theorem which will correct the
7685type error. Idris tells us we have two proof obligations, with names