Lightweight syntax to reuse binding in refined type?

Stream: lean4

[Phil Nguyen]

Suppose I have this simple function that promises to return a Nat thats 1-more:

def inc : (m : Nat) → {n : Nat // n = m + 1}
| m => ⟨m + 1, by simp⟩

Now suppose I want to add a silly requirement that m > 0. The m in the range stops referring to the argument:

def inc' : {m : Nat // m > 0} → {n : Nat // n = m + 1}
| m => ⟨m + 1, by simp⟩ -- fails

I can fix it by somewhat heavyweight syntax:

def inc'' : (m_pos : {m : Nat // m > 0}) → {n : Nat // n = m_pos.val + 1}
| m => ⟨m + 1, by simp⟩

Is there some lightweight syntax to use the same binding both for the argument's refinement and in other places that depend on it?

Many thanks!!

[James Gallicchio]

Not that I'm aware of :/ this could of course be solved via some specialized elaborator support, but I don't think anything like that exists.

I think the standard solution is to just pass hypotheses unpacked (i.e. (m : Nat) -> m > 0 -> ...). I agree it's not the most satisfying solution.

[James Gallicchio]

fwiw, I'd support adding (m : Nat // m > 0) as a binder notation that is elaborated to (m : {m : Nat // m > 0}). Small change but does make it much more readable IMO.

[Kyle Miller]

On the other hand, common wisdom is that it's better to curry your functions. The argument {m : Nat // m > 0} is just waiting to be curried!

[Kyle Miller]

(I've had this same idea for // with binders before. It'd be fun to be able to experiment with these sorts of extensions, but binder syntax is sadly not extensible.)