Notation for subtype arguments

Stream: new members

[Markus Schmaus]

I've been playing around with functions on subtypes and I noticed when I want to have arguments from a subtype I end up typing things like
(n : {n : ℕ // 2 ∣ n}), which awkwardly repeats n :. Is there a better notation for this? I've been considering writing a macro which translates (n : ℕ // 2 ∣ n), into the previous form, would this be a good idea?

Here is a mwe:

import Mathlib

def trueDiv (n : {n : ℕ // 2 ∣ n}) : ℕ := n / 2

PS: Is new members the right place to ask this question?

[Eric Wieser]

Another option here is def trueDiv (n : Subtype (2 ∣ ·)) : ℕ := n / 2, though I'm not sure if it's better

[Anatole Dedecker]

I guess we could have a special syntax for arguments, (n : Nat // 2 | n) does look quite clean to me. In the mean time, your best option is probably to give a name to your subtype if you use it repeatedly

[Yaël Dillies]

Such syntax was already talked about (cc @Kyle Miller). I'm personally in favour of it.

[Jireh Loreaux]

That looks nice.

[Somo S.]

A while back, I proposed syntax
n : {// 2 ∣ ·} for this
(which, IMO, is the most succinct and consistent).

[Somo S.]

At the time, it was suggested that perhaps there is not enough of an advantage to adding such syntax to lean itself, so maybe not worthwhile to add upstream.. Anyway, @Kyle Miller hacked together a quick implementation of it which inspired me to write it into a little convenience library (called Supertype ) that I use for my own projects where I want this feature.

[Somo S.]

The next thing I'd like to explore in Supertype is incorporating "destructured" pattern match syntax like:

{(a,b) // 5 ≤ a + b}

which, in this case, would be exactly the same as:

Subtype fun (a,b) => 5 ≤ a + b

[Somo S.]

"destructured" pattern match syntax like {(a,b) // 5 ≤ a + b}

I continued pursuing this over here:
https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/.E2.9C.94.20destructured.20subtype.20pattern-match.20syntax