New-user question: what's the best way to express types with a lot of dependent information? I've been using specifications, which are great when you have a single condition or a single extra piece of data, but they start to get really verbose when you have a lot of data types all depending on each other.
For example, I'm trying to formalize a Boolean circuit, which is something like: "a DAG with a function that maps nodes of the DAG to gate types, such that exactly n of those gates are input gates, and those input gates have a function to the naturals that is injective over the first n naturals..." etc.
I guess the nominal answer is: a dependent record. But that is not the end of the story. Whether the record should be declared as a type class or whatever should be discussed. But you should definitely start with a record.
That looks like exactly what I was looking for. Thanks! I'll give it a try.
Jake has marked this topic as resolved.
Last updated: Oct 03 2023 at 20:01 UTC