determine whether type is enumerated

Stream: lean4

[Calvin Lee]

Is there any way to check if a type is "Enumerated" as described in the lean4 manual when performing term elaboration?
I would like to write a deriving rule for ToJson/FromJson for "Enumerated" types, similar to how there is one for structures, but I am having a hard time figuring out how to make sure a type satisfies these conditions.

[Sebastian Ullrich]

This is part of the compiler that has yet to be translated to Lean, but the implementation is simple enough (and you might want to adapt it to your needs anyway): https://github.com/leanprover/lean4/blob/master/src/library/compiler/util.cpp#L30

[Calvin Lee]

Hm, is there any information about how I could write a new deriving rule? I've been reading through the term elaboration code quite a bit.
Is this something that would have to occur in the compiler? Or could i write it in my project?