属性紹介: @[class] 属性

[Seasawher]

see: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/what.20is.20.60class.60.20attribute/near/445581181

MIL の７章に記述があるものの，ただの構造体との違いがわからない

[Seasawher]

variable {α : Type}

@[class] structure One (α : Type) where
  one : α

instance instOneNat : One Nat where
  one := 1

structure Two (α : Type) where
  two : α

instance instTwoNat : Two Nat where
  two := 2

example {T : Type} [One T] : True := by trivial

/--
error: invalid binder annotation, type is not a class instance
  Two T
use the command `set_option checkBinderAnnotations false` to disable the check
-/
#guard_msgs in example {T : Type} [Two T] : True := by trivial

#synth One Nat

/--
error: type class instance expected
  Two Nat
-/
#guard_msgs in #synth Two Nat