git.iko.soy/Idris-dev
on master help sign in
Clarify parity/natToBin in the tutorial
b932c1bEdwin Brady
tutorial/provisional.tex+15
compare with master
unifiedsplit
@@ -1,5 +1,7 @@
1\section{Provisional Definitions}
1\section{Provisional Definitions}
2
2
3+\label{sect:provisional}
4+
3Sometimes when programming with dependent types, the type required by the type
5Sometimes when programming with dependent types, the type required by the type
4checker and the type of the program we have written will be different (in that
6checker and the type of the program we have written will be different (in that
5they do not have the same normal form), but nevertheless provably equal. For
7they 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
195\texttt{value} in the premisses. The proof of the second lemma proceeds in
197\texttt{value} in the premisses. The proof of the second lemma proceeds in
196exactly the same way.
198exactly the same way.
197
199
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+
198\subsection{Suspension of Disbelief}
213\subsection{Suspension of Disbelief}
199
214
200\Idris{} requires that proofs be complete before compiling programs (although
215\Idris{} requires that proofs be complete before compiling programs (although
tutorial/views.tex+4−10
@@ -75,6 +75,8 @@ parity : (n:Nat) -> Parity n
75\end{SaveVerbatim}
75\end{SaveVerbatim}
76\useverb{parityty}
76\useverb{parityty}
77
77
78+\label{sect:nattobin}
79+
78\noindent
80\noindent
79We'll come back to the definition of \texttt{parity} shortly. We can use it
81We'll come back to the definition of \texttt{parity} shortly. We can use it
80to write a function which converts a natural number to a list of binary digits
82to 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} ---
103this is allowed
105this is allowed
104because another argument has determined the form of these patterns.
106because another argument has determined the form of these patterns.
105
107
106−We can test this function at the prompt. 42 is 101010 in binary. The binary digits
108+We will return to this function in Section \ref{sect:provisional} to complete
107−are reversed with natToBin:
109+the definition of \texttt{parity}.
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}
116
110
117
111