属性紹介: @[class] 属性

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

lean-ja / lean-by-example

属性紹介: @[class] 属性 #309