[Agda] `divides' definition

Sergei Meshveliani mechvel at botik.ru
Tue Jun 4 13:18:13 CEST 2013


People,

the Standard lib-0.7 defines

  data _∣_ : ℕ → ℕ → Set where
    divides : {m n : ℕ} (q : ℕ) (eq : n ≡ q * m) → m ∣ n

Why does not it use the existing library constructor of `∃' by defining

  _∣_ : Rel ℕ Level.zero
  m ∣ n = ∃ \ q → (q * m ≡ n)
 
?

Thanks,

------
Sergei



More information about the Agda mailing list