Introduce names for parts of types refined by patterns

Stream: new members

[hakanaras]

Let's say I pattern match on something and discover that it's type's parameters have a specific form. How do I introduce names for the parts of that new form?

inductive I : (i : Nat) -> Type where
  | a : I 0
  | b : (n : Nat) -> I i -> I (i + 1 + n)

def f {i : Nat} : I i -> Nat
  | .a => 0
  | .b n rest =>
      -- I know that `i` has the form `i✝ + 1 + n`.
      -- How can I introduce a name for that `i✝`?
      sorry

[Eric Paul]

The following gives you access to an i' which I think is what you are looking for. Since the i is an implicit argument to b, we can use the @ syntax to make everything explicit and thus name that argument.

inductive I : (i : Nat) -> Type where
  | a : I 0
  | b : (n : Nat) -> I i -> I (i + 1 + n)

def f {i : Nat} : I i -> Nat
  | .a => 0
  | @I.b i' n rest => by
      sorry

Another option would be to make the i argument to b explicit in its definition as follows:

inductive I : (i : Nat) -> Type where
  | a : I 0
  | b (i) : (n : Nat) -> I i -> I (i + 1 + n)

def f {i : Nat} : I i -> Nat
  | .a => 0
  | .b i' n rest => by
      sorry

[hakanaras]

I see, thanks.