Zulip Chat Archive

Stream: new members

Topic: Invalid binder annotation

YurySerdyuk (Jul 17 2023 at 13:45):

What is wrong with my Lean4 code using Field type:

variable {𝕜 : Type} {M : Type}
variable [DecidableEq 𝕜] [Field 𝕜]

invalid binder annotation, type is not a class instance

for [Field 𝕜] attribute.

Alex J. Best (Jul 17 2023 at 13:56):

What are your imports, can you give us a #mwe? You'll need to import some of mathlib to talk about fields for sure

Kyle Miller (Jul 17 2023 at 13:57):

This error looks like the auto-implicits feature is kicking in, which makes it hard to see that you don't have Field imported. For a better experience, try putting set_option relaxedAutoImplicit false at the top of your file, after the imports.

Last updated: Dec 20 2023 at 11:08 UTC