Stream: Coq users

Topic: ✔ Extracting record type

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.

Julin S (Aug 25 2022 at 04:11):

Should it be like an inductive type?

Paolo Giarrusso (Aug 25 2022 at 04:18):

You might need Extract Inductive?

Paolo Giarrusso (Aug 25 2022 at 04:20):

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

Julin S (Aug 25 2022 at 04:24):

Using the Extract Inductive worked. Thanks!

Notification Bot (Aug 25 2022 at 04:24):

Julin S has marked this topic as resolved.

Last updated: Sep 23 2023 at 07:01 UTC