git.iko.soy/Idris-dev
on master help sign in
Clarify parity/natToBin in the tutorial

Fixes #583

commitb932c1bca733487d912ce18cb6cab9d590778a57 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 3 Nov 2013, 12:36 (13 years ago) parent6b3457a
2 files changed+19−10
compare with master
unifiedsplit
tutorial/provisional.tex+15 tutorial/views.tex+4−10
tutorial/provisional.tex+15
@@ -1,5 +1,7 @@
11\section{Provisional Definitions}
22
3+\label{sect:provisional}
4+
35Sometimes when programming with dependent types, the type required by the type
46checker and the type of the program we have written will be different (in that
57they do not have the same normal form), but nevertheless provably equal. For
@@ -195,6 +197,19 @@ We can complete this proof using the \texttt{trivial} tactic, which finds
195197\texttt{value} in the premisses. The proof of the second lemma proceeds in
196198exactly the same way.
197199
200+We can now test the \texttt{natToBin} function from Section
201+\ref{sect:nattobin} at the prompt. 42 is 101010 in
202+binary. The binary digits are reversed:
203+
204+\begin{SaveVerbatim}{ntbtest}
205+
206+*views> show (natToBin 42)
207+"[False, True, False, True, False, True]" : String
208+
209+\end{SaveVerbatim}
210+\useverb{ntbtest}
211+
212+
198213\subsection{Suspension of Disbelief}
199214
200215\Idris{} requires that proofs be complete before compiling programs (although
tutorial/views.tex+4−10
@@ -75,6 +75,8 @@ parity : (n:Nat) -> Parity n
7575\end{SaveVerbatim}
7676\useverb{parityty}
7777
78+\label{sect:nattobin}
79+
7880\noindent
7981We'll come back to the definition of \texttt{parity} shortly. We can use it
8082to write a function which converts a natural number to a list of binary digits
@@ -103,15 +105,7 @@ function in the patterns (\texttt{+}) and repeated occurrences of \texttt{j} ---
103105this is allowed
104106because another argument has determined the form of these patterns.
105107
106−We can test this function at the prompt. 42 is 101010 in binary. The binary digits
107−are reversed with natToBin:
108−
109−\begin{SaveVerbatim}{ntbtest}
110−
111−*views> show (natToBin 42)
112−"[False, True, False, True, False, True]" : String
113−
114−\end{SaveVerbatim}
115−\useverb{ntbtest}
108+We will return to this function in Section \ref{sect:provisional} to complete
109+the definition of \texttt{parity}.
116110
117111