Confusion about pattern-matching

Stream: general

[Valentin Robert]

Hello,

I'm trying Lean, and have been confused by the following, rather simple code:

inductive x : Type
| mkx (f : ℕ → x) : x

def catax : x → ℕ
| mkx := 0

This works, but if I try and write (mkx f) for the pattern in catax, I get the following error:

equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
invalid application, function expected

I feel like I have done other pattern-matches elsewhere where the opposite was true, so am I doing something silly here that I'm not noticing?

[Marc Huisinga]

This works for me:

inductive x : Type
| mkx (f : ℕ → x) : x

def catax : x → ℕ
| (x.mkx f) := 0

[Patrick Massot]

To be more explicit: this is a namespacing issue. You can also type open x between your two declarations.

[Valentin Robert]

Huh, of course!
So in my working example, mkx in the pattern is just a binding catch-all pattern? :D