Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
branch: master
Fetching contributors…

Cannot retrieve contributors at this time

18 lines (15 sloc) 0.434 kb
module NatCmp
{-
data Cmp : Nat -> Nat -> Type where
cmpLT : (y : _) -> Cmp x (x + S y)
cmpEQ : Cmp x x
cmpGT : (x : _) -> Cmp (y + S x) y
total cmp : (x, y : Nat) -> Cmp x y
cmp Z Z = cmpEQ
cmp Z (S k) = cmpLT _
cmp (S k) Z = cmpGT _
cmp (S x) (S y) with (cmp x y)
cmp (S x) (S (x + (S k))) | cmpLT k = cmpLT k
cmp (S x) (S x) | cmpEQ = cmpEQ
cmp (S (y + (S k))) (S y) | cmpGT k = cmpGT k
-}
Jump to Line
Something went wrong with that request. Please try again.