| module | |
| /-! Applying `[instance]` after the fact should check for appropriate reducibility. -/ | |
| /-- | |
| warning: Definition `unexposed` of class type must be marked with `@[reducible]`, `@[instance_reducible]`, `@[implicit_reducible]` or `@[irreducible]` | |
| -/ | |
| #guard_msgs in | |
| public def unexposed : Inhabited Nat := inferInstance | |
| /-- warning: instance `unexposed` must be marked with `@[expose]` -/ | |
| #guard_msgs in | |
| attribute [instance] unexposed | |
| /-- | |
| warning: instance `unexposed` must be marked with `@[reducible]`, `@[instance_reducible]` or `@[implicit_reducible]` | |
| -/ | |
| #guard_msgs in | |
| attribute [local instance] unexposed | |
| /-- | |
| warning: Definition `exposed` of class type must be marked with `@[reducible]`, `@[instance_reducible]`, `@[implicit_reducible]` or `@[irreducible]` | |
| -/ | |
| #guard_msgs in | |
| @[expose] | |
| public def exposed : Inhabited Nat := inferInstance | |
| /-- | |
| warning: instance `exposed` must be marked with `@[reducible]`, `@[instance_reducible]` or `@[implicit_reducible]` | |
| -/ | |
| #guard_msgs in | |
| attribute [instance] exposed | |
| /-- | |
| warning: instance `exposed` must be marked with `@[reducible]`, `@[instance_reducible]` or `@[implicit_reducible]` | |
| -/ | |
| #guard_msgs in | |
| attribute [local instance] exposed | |
| @[expose, instance_reducible] | |
| public def exposedAndReducible : Inhabited Nat := inferInstance | |
| #guard_msgs in | |
| attribute [instance] exposedAndReducible | |
| #guard_msgs in | |
| attribute [local instance] exposedAndReducible | |
| instance bla : Add Int := ⟨Int.add⟩ | |
| #guard_msgs in | |
| attribute [irreducible] bla |