Stream: Coq users

Topic: Auxiliary definitions during record definition?


view this post on Zulip Joshua Grosso (Sep 10 2021 at 02:20):

I'm trying to define a (dependent) record type where writing the types of the later fields would be much easier if I could create and use definitions/notations/etc. that depend on some of the earlier fields. Is this (or something with a similar effect, e.g. using modules) possible?

view this post on Zulip Matthieu Sozeau (Sep 10 2021 at 11:15):

You can use local field definitions foo := bar; directly in your record definition

view this post on Zulip Matthieu Sozeau (Sep 10 2021 at 11:16):

I think you can use where "notation" also, but you'll have to check the grammar

view this post on Zulip Joshua Grosso (Sep 11 2021 at 00:22):

Thanks! Out of curiosity, is it possible to use Program functionality in these fields (#[program] Record didn't seem to work)?


Last updated: Feb 01 2023 at 12:30 UTC