8 lines
162 B
Text
8 lines
162 B
Text
@[derive [decidable_eq, inhabited, has_sizeof]]
|
||
inductive foo
|
||
| bar : ℕ → foo
|
||
| baz : foo
|
||
|
||
#check foo.decidable_eq
|
||
#check foo.inhabited
|
||
#check foo.has_sizeof
|