Stream: Coq users

Topic: Extraction Singleton for specific types


view this post on Zulip Josh Cohen (Mar 26 2024 at 16:29):

Is there a way to specify that only certain 1-constructor ADTs should be inlined, rather than all (with the Extraction KeepSingleton flag)?


Last updated: Oct 13 2024 at 01:02 UTC