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