idris - Why can (and must) the variable x appear twice on the left side of the function definition? And what's the meaning?

Question

I'm a green hand with Idris,and get confused with this definition, as I don't understand how it works. The definitionare as follows.

sameS : (k : Nat)->(j : Nat)->(k = j)->((S k) = (S j))
sameS x x Refl=Refl

Answer 1

Let us start by breaking down the type signature:

sameS : (k : Nat) -> (j : Nat) -> (k = j) -> ((S k) = (S j))

sameS is a function. sameS take the following arguments:

1. (k : Nat) a parameter k of type Nat
2. (j : Nat) a parameter j of type Nat
3. (k = j) A proof that k and j are equal

sameS returns:

((S k) = (S j)) proof that S k and S j are equal.

Now let us breakdown the definition:

sameS x x Refl = Refl

The type of Refl is a = a.

x is both the first and second argument because both are identical. We know this because the 3rd argument is Refl.

Refl is returned because S x = S x.