data.bitvec.core mathlib4#1731

Stream: mathlib4

[Shreyas Srinivas]

I encountered an error in the following:

/-- bitwise not -/
def not : Bitvec n → Bitvec n :=
  map not
#align bitvec.not Bitvec.not

/-- bitwise and -/
def and : Bitvec n → Bitvec n → Bitvec n :=
  map₂ and
#align bitvec.and Bitvec.and

/-- bitwise or -/
def or : Bitvec n → Bitvec n → Bitvec n :=
  map₂ or
#align bitvec.or Bitvec.or

/-- bitwise xor -/
def xor : Bitvec n → Bitvec n → Bitvec n :=
  map₂ xor
#align bitvec.xor Bitvec.xor

[Shreyas Srinivas]

in each instance the boolean operation say not was being interpreted as Bitvec.not inside the def. This seems to be an error in the type inference.

[Shreyas Srinivas]

I can't fix this by introducing explicit arguments, but if I recall my haskell experience, the type inference algorithm would have taken care of it

[Shreyas Srinivas]

Why is this happening?

[Shreyas Srinivas]

and what is the lean4 fix?

[Reid Barton]

_root_.not etc should work, or Bool.not or whatever the right name is

[Eric Wieser]

nonrec def should also fix it

[Reid Barton]

Ah nice, I have encountered this also in non-mathlib contexts and that could have been useful to know.

[Kevin Buzzard]

Shreyas Srinivas said:

Why is this happening?

It's because his is how Lean 4 works: priority goes to what you're currently defining. Whether that's a good idea is another question.

[Notification Bot]

24 messages were moved from this topic to #mathlib4 > nonrec vs _root_ by Eric Wieser.