new to Lean 4: sorryAx?

Stream: new members

[Paula Neeley]

I've looked at the documentation for sorryAx, but it's not helping to clarify why I'm getting it here. Can somebody please ELI5?

import Std.Data.BitVec.Basic

variable (bv32 : BitVec 32)
#check bv32

[Ruben Van de Velde]

Looks like it doesn't recognise docs#BitVec because it's actually Std.BitVec

[Paula Neeley]

Ruben Van de Velde said:

Looks like it doesn't recognise docs#BitVec because it's actually Std.BitVec

Thank you, prefixing it with Std fixed the issue

[Eric Wieser]

Note that set_option autoImplicit false would have given you a better error message

[Mario Carneiro]

Actually I don't think this is an autoImplicit issue, this is lean4#2226 (variable eats errors without reporting)

[Mario Carneiro]

note that

set_option autoImplicit true
set_option relaxedAutoImplicit true
example (bv32 : BitVec 32) : True := trivial

fails

[Ashley Blacquiere]

I had asked a question about BitVec on another thread, so this caught my eye.

I stuck the example above into my code and noticed something that seems odd:

import Mathlib.Probability.ProbabilityMassFunction.Basic

namespace Std

variable (bv32 : BitVec 32)
#check bv32

The above works fine, but should it? I haven't imported Std directly, but I'm able to open the namespace as long as import Mathlib.Probability.ProbabilityMassFunction.Basic. If I comment out only the import statement I end up with an error onBitVec... Seems weird that that import would also make Std available, no?

[Damiano Testa]

Imports are transitive, so, to me, it does not seem particularly strange. I would definitely say that this is expected.