@@ -71,6 +71,15 @@ Provisional definitions are written in the same way as ordinary
71definitions, except that they introduce the right hand side with a
71definitions, except that they introduce the right hand side with a
72``?=`` rather than ``=``. We define ``parity`` as follows:
72``?=`` rather than ``=``. We define ``parity`` as follows:
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}
74When written in this form, instead of reporting a type error, Idris
83When written in this form, instead of reporting a type error, Idris
75will insert a metavariable standing for a theorem which will correct the
84will insert a metavariable standing for a theorem which will correct the
76type error. Idris tells us we have two proof obligations, with names
85type error. Idris tells us we have two proof obligations, with names