Joshua Grosso (Sep 10 2021 at 02:20): 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?
Matthieu Sozeau (Sep 10 2021 at 11:15):You can use local field definitions foo := bar; directly in your record definition
Matthieu Sozeau (Sep 10 2021 at 11:16):I think you can use where "notation" also, but you'll have to check the grammar
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: Sep 23 2023 at 14:01 UTC