Stream: Coq users

Topic: ✔ Extracting record type


view this post on Zulip Julin S (Aug 25 2022 at 04:10):

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.

view this post on Zulip Julin S (Aug 25 2022 at 04:11):

Should it be like an inductive type?

view this post on Zulip Paolo Giarrusso (Aug 25 2022 at 04:18):

You might need Extract Inductive?

view this post on Zulip Paolo Giarrusso (Aug 25 2022 at 04:20):

"Constant" means specifically definitions introduced by Definition, or derived concepts like Fixpoint

view this post on Zulip Julin S (Aug 25 2022 at 04:24):

Using the Extract Inductive worked. Thanks!

view this post on Zulip Notification Bot (Aug 25 2022 at 04:24):

Julin S has marked this topic as resolved.


Last updated: Feb 01 2023 at 11:04 UTC