[Agda] `divides' definition

[Nils Anders Danielsson]

On 2013-06-04 13:18, Sergei Meshveliani wrote:
> 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)
>
> ?

IIRC I used to prefer the former kind of definition. If I rewrote the
definition today I would probably use a Σ-type.

-- 
/NAD