c613fab · Idris-dev · git.iko.soy

tutorial/examples/binary.idr+1−1

@@ -34,7 +34,7 @@ intToNat x = if (x>0) then (S (intToNat (x-1))) else O

34main : IO ()

35main = do putStr "Enter a number: "

36 x <- getLine

37− print $ natToBin (fromInteger (cast x))

37+ print (natToBin (fromInteger (cast x)))

38

39---------- Proofs ----------

40

tutorial/idris-tutorial.pdf

Binary file not shown.

tutorial/provisional.tex+1−2

@@ -284,8 +284,7 @@ outputs it in binary.

284main : IO ()

285main = do putStr "Enter a number: "

286 x <- getLine

287− let b = natToBin (fromInteger (cast x))

287+ print (natToBin (fromInteger (cast x)))

288− print b

289

288

290\end{SaveVerbatim}

289\end{SaveVerbatim}

291\useverb{binmain}

290\useverb{binmain}