module Division where open import Bool open import Nat -- cut-off subtraction _-_ : Nat → Nat → Nat zero - n = zero succ m - zero = succ m succ m - succ n = m - n -- less than or equal _<=_ : Nat → Nat → Bool zero <= n = true succ m <= zero = false succ m <= succ n = m <= n -- if then else for Nat ifn_then_else_ : Bool → Nat → Nat → Nat ifn true then y else z = y ifn false then y else z = z -- division by repeated subtraction {-# NON_TERMINATING #-} _÷_ : Nat → Nat → Nat -- m ÷ zero = zero m ÷ n = ifn m <= n then zero else succ ((m - n) ÷ n) {-# NON_TERMINATING #-} loop : Nat loop = loop