equation compiler and dependent types

Stream: general

[Patrick Massot]

Is there any way to use the equation compiler with a dependent output? The following works (although I wish the proof part could be by linarith):

def euclid : ℕ → { n : ℕ | 0 < n } → ℕ × ℕ
| m n := if h : m < n then
           (0, m)
         else
           have (0 : ℕ) < n, from n.property,
           have m - n < m, by apply nat.sub_lt ; linarith,
           let ⟨q, r⟩ := euclid (m-n) n in ⟨q+1, r⟩

But now suppose I want the output type to be { p : ℕ × ℕ | m = n*p.1 + p.2 ∧ p.2 < n}. Is something like this possible? Of course here Lean complains it doesn't know who are m and n, which will appear only after matching. Of course I also wish I could write { (q, r) : ℕ × ℕ | m = n*q + r ∧ r < n} (or with angle brackets)instead of those ugly p.1 and p.2, but at least this is not blocking.

[Patrick Massot]

Sorry about this stupid question

[Patrick Massot]

I can use a Pi type instead

[Patrick Massot]

Note for next time I ask: one possible answer is

def euclid : Π (m : ℕ) (n : { n : ℕ // 0 < n }), {p : ℕ × ℕ // m = n*p.1 + p.2 ∧ p.2 < n}
| m n := if h : m < n then
           ⟨(0, m), by simp *⟩
         else
           have (0 : ℕ) < n, from n.property,
           have m - n < m, by apply nat.sub_lt ; linarith,
           let ⟨⟨q, r⟩, ⟨H, H'⟩⟩ := euclid (m-n) n in
             ⟨(q+1, r),
              ⟨begin
                rw nat.sub_eq_iff_eq_add (le_of_not_lt h) at H,
                simp [H], ring,
               end, H'⟩⟩