This is similar (but not the same) as #551 . I don't I've submitted this before.
I've been using variants to represent optional givens, for example:
given neighbourhood_CLUES : variant {
None, Some_CLUES : record { Min: int, Max: int, Val_CLUES: int }
}
given neighbourhood_GRID : variant {
None, Some_GRID : record { Min: int, Max: int, Val_GRID: matrix indexed by [int, int] of int }
}
I would prefer to use just Some and Val, but then I'm told I can't reuse the name. I don't know how easy it would be to let names be reused, but I thought I'd mention the irritation.
This is similar (but not the same) as #551 . I don't I've submitted this before.
I've been using variants to represent optional givens, for example:
I would prefer to use just
Some
andVal
, but then I'm told I can't reuse the name. I don't know how easy it would be to let names be reused, but I thought I'd mention the irritation.