How about making _|_ a record instead of a datatype?

[gallais]

The notion of divisibility is defined using a datatype which makes it
impossible to pattern match against a proof that m | n in a let-binding.

I suggest using the following record-based definition instead:

record _∣_ (m n : ℕ) : Set where
  constructor divides
  field quotient : ℕ
        equality : n ≡ quotient * m

However this will break some proofs: for some reasons m and n were not
declared as parameters of _|_ but rather as indices. This means that the
divides constructor was carrying them as implicit arguments and this is used
in the standard library (see e.g. ∣-antisym).

Any opposition to the breaking change?

[asr]

I couldn't find any difference using both definitions (the data type and the record). Could you write-down a MWE?

[gallais]

The following definition only works if m ∣ n is defined as a record:

extract : {m n : ℕ} → m ∣ n → ℕ
extract pr = let (divides q _) = pr in q

[andreasabel]

The only reason I see for a data type here is printing. But this should not stop us...

[MatthewDaggitt]

Closed with eeb0690