Elaboration of `≠`

Stream: lean4

[Aaron Liu]

Is ≠ not a binrel%?

def k : Int := 0

def l : Nat := 0

/--
info: ↑l = k : Prop
-/
#guard_msgs in
#check l = k

/--
error: Application type mismatch: In the application
  l ≠ k
the argument
  k
has type
  Int : Type
but is expected to have type
  Nat : Type
---
info: l ≠ sorry : Prop
-/
#guard_msgs in
#check l ≠ k

I think we should aim to make what = and ≠ do here match as closely as possible.

[Jz Pan]

That's strange. l ≤ k and l < k works correctly.

[Kenny Lau]

Maybe it's because it's an abbrev (and I hate abbrevs, lol)

[Aaron Liu]

It's not because it's an abbrev

[Aaron Liu]

Is because it's not a binrel%

[Aaron Liu]

def k : Int := 0

def l : Nat := 0

-- fails
#check Eq l k

-- succeeds (this is what `l = k` expands to)
#check binrel% Eq l k

-- fails (this is what `l ≠ k` expands to)
#check Ne l k

-- succeeds
#check binrel% Ne l k

[Kyle Miller]

Jz Pan said:

l ≤ k and l < k works correctly.

These both have binrel% macros

[Kyle Miller]

@Aaron Liu I imagine it's an oversight, since ≠ isn't defined in Init.Notation

[Kyle Miller]

Feel free to create a Lean PR adding such a binrel% macro to Init.Core and ping me once mathlib builds.