PDF cleanup 282: hide module syntax
#370
Conversation
This addresses one item of issue #282.
| \begin{code} | ||
| module _ (khs : ℙ KeyHash) (I : Maybe Slot × Maybe Slot) where |
There was a problem hiding this comment.
Since this module block contains only one thing, I think it'd be better to just add these as arguments to the datatype.
There was a problem hiding this comment.
Oh gosh, the repetition...
Also isn't it more confusing now to have the readers read "indexed constant types"?
There was a problem hiding this comment.
Is there any repetition?
Generally I agree, but I think presenting evalTimelock as a datatype is a bad idea in the first place (why isn't it a function?). So when we have a spec that actually wants to present this there's a decent chance that we'll want to refactor this anyway.
There was a problem hiding this comment.
The repetition comes from the "constant" indices, s/evalTimelock/(evalTimelock khs I), which is why I used module parameters as the best practice to avoid this, and results in much more readable constructors.
Having said that, I agree that using the "call-graph view" of the function as a datatype might be a bit too much here, I don't know why Ali initially did it this way. I agree you should investigate the alternative sooner rather than later to avoid maintenance overhead.
Description
This addresses one item of issue #282.
Checklist