Zulip Chat Archive

Stream: lean4

Topic: determine whether type is enumerated


view this post on Zulip Calvin Lee (Feb 28 2021 at 06:18):

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.

view this post on Zulip Sebastian Ullrich (Feb 28 2021 at 08:31):

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

view this post on Zulip Calvin Lee (Mar 02 2021 at 06:00):

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?


Last updated: May 18 2021 at 23:14 UTC