← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to examples/outdated-and-incorrect/AIM6/Cat/lib/Data/Bits.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/outdated-and-incorrect/AIM6/Cat/lib/Data/Bits.agda
1
 
 
2
 
module Data.Bits where
3
 
 
4
 
import Prelude
5
 
import Logic.Base
6
 
import Data.List as List
7
 
import Data.Nat  as Nat
8
 
import Data.Bool as Bool
9
 
 
10
 
open Prelude
11
 
open Nat
12
 
open Bool
13
 
open List
14
 
 
15
 
Bit = Bool
16
 
 
17
 
shiftL : Nat -> Nat -> Nat
18
 
shiftL n i = n * 2 ^ i
19
 
 
20
 
sucBits : List Bit -> List Bit
21
 
sucBits []            = true :: []
22
 
sucBits (false :: xs) = true :: xs
23
 
sucBits (true  :: xs) = false :: sucBits xs
24
 
 
25
 
toBits : Nat -> List Bit
26
 
toBits zero    = []
27
 
toBits (suc n) = sucBits (odd n :: toBits (div n 2))
28
 
 
29
 
fromBits : List Bit -> Nat
30
 
fromBits xs = foldr (\b n -> bitValue b + 2 * n) 0 xs
31
 
  where
32
 
    bitValue : Bit -> Nat
33
 
    bitValue b = if b then 1 else 0
34
 
 
35
 
nofBits : Nat -> Nat
36
 
nofBits = length ∘ toBits
37
 
 
38
 
module Proofs where
39
 
 
40
 
  open Logic.Base
41
 
 
42