How can we create mapping to target language for extracting a record type?
When I tried to do like:
Extract Constant RecType => "rectype".
Coq complained saying:
RecType is not a constant.
Should it be like an inductive type?
You might need
"Constant" means specifically definitions introduced by
Definition, or derived concepts like
Extract Inductive worked. Thanks!
Julin S has marked this topic as resolved.
Last updated: Feb 01 2023 at 11:04 UTC