How to combine Subtype and pairs?

Stream: new members

[Jakub Nowak]

Is there a syntax to combine pairs and Subtype? Something like { ⟨n, m⟩ : Nat × Nat // n+1 = m } or { n m : Nat // n+1 = m }.
I probably should make structure anyway, but just wanted to ask.

[Chris Bailey]

The syntax for Subtype requires the thing on the left to be an ident, so it doesn't seem that such a pattern will work:

@[inherit_doc Subtype] syntax "{ " withoutPosition(ident (" : " term)? " // " term) " }" : term

You can of course write a macro, or just do something like { pr : Nat × Nat // pr.fst+1 = pr.snd }

[Dan Velleman]

You can write {(n, m) : Nat × Nat | n+1 = m}, but that gives you a set rather than a Subtype. But you could then coerce it to be a Subtype. Not sure how useful that approach would be.

[Dan Velleman]

Note that the resulting Subtype is equal to Chris's last suggestion:

import Mathlib

example : ↑ {(n, m) : Nat × Nat | n + 1 = m} =
  {pr : Nat × Nat // pr.fst + 1 = pr.snd} := rfl