Module Nat

Meta-data

Contents

data N (n : Nat) where
    Z : N 0
  ; S : (N n) -> N (n + 1)

copyNat : forall {n : Nat} 
        . (N n) -> (N n, N n)

natToInt : forall {n : Nat} 
         . (N n) -> Int
Convert an indexed natural number to an untyped int

[top] Arithmetic operations

add : forall {m : Nat, n : Nat} 
    . (N n) -> (N m) -> N (n + m)
Addition
monus : forall {m : Nat, n : Nat} 
      . (N m) -> (N n) -> N (m - n)

sub : forall {m : Nat, n : Nat} 
    . {n .≥ m} =>
    (N n) -> (N m) -> N (n - m)

mult : forall {m : Nat, n : Nat} 
     . (N n) -> ((N m) [n]) -> N (n * m)
Right-moded multiplication
mult_r : forall {m : Nat, n : Nat} 
       . ((N n) [m]) -> (N m) -> N (n * m)
Left-moded multiplication
div2 : forall {n : Nat} 
     . (N (2 * n)) -> N n
Divide by two