Trouble with basic pattern matching?

Stream: lean4

[Colin Gordon]

I'm trying out lean4, and have managed to run into a problem that makes me think I'm just trying something dumb. I'd really appreciate if someone could get me unstuck.

inductive box : Type
| mk : Nat -> box
def unbox (b:box) : Nat :=
  match b with
  | mk n => n

yields the message:
box.lean:5:4: error: invalid pattern, constructor or constant marked with '[matchPattern]' expected
This isn't what I'm actually trying to do, but I kept minimizing and ended up with this. I'm using a fresh install of Lean (version 4.0.0-m2, commit 26dda3f63d88, Release). Clearly I must be trying to do something the wrong way, though I'm unclear what, as I've been checking what I'm trying to write against tests in the lean4 repository, such as https://github.com/leanprover/lean4/blob/v4.0.0-m2/tests/lean/match1.lean

Thanks to anyone who can help get me sorted out

[Marc Huisinga]

Colin Gordon said:

I'm trying out lean4, and have managed to run into a problem that makes me think I'm just trying something dumb. I'd really appreciate if someone could get me unstuck.

inductive box : Type
| mk : Nat -> box
def unbox (b:box) : Nat :=
  match b with
  | mk n => n

yields the message:
box.lean:5:4: error: invalid pattern, constructor or constant marked with '[matchPattern]' expected
This isn't what I'm actually trying to do, but I kept minimizing and ended up with this. I'm using a fresh install of Lean (version 4.0.0-m2, commit 26dda3f63d88, Release). Clearly I must be trying to do something the wrong way, though I'm unclear what, as I've been checking what I'm trying to write against tests in the lean4 repository, such as https://github.com/leanprover/lean4/blob/v4.0.0-m2/tests/lean/match1.lean

Thanks to anyone who can help get me sorted out

I think the right input here is box.mk instead of mk in the match

[Marc Huisinga]

but you might also want to use the nightlies instead of the stable release (which is quite old in comparison)

[Colin Gordon]

Thanks! That does indeed fix that, and now I'm off to go debug a universe issue in what I was originally trying to do. I'm curious though, why there are cases in the tests that work without those qualifications, such as

def Sum.str : Option Nat → String :=
  fun
    | some a => "some " ++ toString a
    | none   => "none"

which typechecks just fine without using Option.some etc.

[Yakov Pechersky]

Because some and none are exported to be in the global namespaces. You can also say "open box" to open that namespace, or say "open box in def ..." to open it solely local to the body of the definition

[Marc Huisinga]

cf. https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L985 and the corresponding docs for lean 3 where it works the same way: https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html?highlight=export#more-on-namespaces

[Colin Gordon]

Thanks, both of you!