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?
You can use local field definitions
foo := bar; directly in your record definition
I think you can use
where "notation" also, but you'll have to check the grammar
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