Matching over integers

Stream: lean4

[Son Ho]

I'm trying to write matches over integers. The following works:

def is_one (x : ℤ) : Bool :=
  match x with
  | 1 => true
  | _ => false

However, I have a syntax error here (invalid pattern, constructor or constant marked with '[match_pattern]' expected):

def is_minus_one (x : ℤ) : Bool :=
  match x with
  | -1 => true
  | _ => false

Is there something I can do to make Lean accept this definition? In particular, I'm not sure how the -1 is elaborated.

[Jannis Limperg]

This works:

def is_minus_one (x : Int) : Bool :=
  match x with
  | -1 => true
  | _ => false

#eval is_minus_one (-1) -- true
#eval is_minus_one (-2) -- false
#eval is_minus_one (3)  -- false

Note Int instead of ℤ. ℤ is a Mathlib notation, so maybe it just wasn't imported.

[Son Ho]

This is strange, it still doesn't work on my side. Maybe it is because on the contrary I imported too many things from mathlib?

[Eric Rodriguez]

Can you post a file where it doesn't work?

[Son Ho]

Yes, I'm currently minimizing it

[Son Ho]

The problem comes from the fact that I introduced a "heterogeneous negation" typeclass, with the corresponding notation.

import Lean

class HNeg (α : Type u) (β : outParam (Type v)) where
  hNeg : α → β

prefix:75  "-"   => HNeg.hNeg

def is_minus_one (x : Int) : Bool :=
  match x with
  | -1 => true
  | _ => false

So my question becomes (sorry for the noise): how can I introduce the notation above without breaking the is_minus_one example?

[Jannis Limperg]

Then you have to add the match_pattern attribute. This tells Lean that an arbitrary function (here HNeg.hNeg) is allowed to appear in patterns.

class HNeg (α : Type u) (β : outParam (Type v)) where
  hNeg : α → β

prefix:75  "-"   => HNeg.hNeg

attribute [match_pattern] HNeg.hNeg

def is_minus_one (x : Int) : Bool :=
  match x with
  | -1 => true
  | _ => false

[Son Ho]

Perfect, thanks Jannis! :)