google-research
Got sets working with new syntax and fixed tests.
Still getting used to the new restrictive type inference.
One minor sadness is that I wasn't able to strengthen the type of Element as much as in one of the old PRs. Specifically,
struct Element(set:(Set a)) given (a|Ord) =
val: Nat # Could be (Fin (set_size set))
For a long time Dex couldn't handle a function call inside a type definition, then it could for a while, now it can't again.
Anyways, you told me to complain!
For a long time Dex couldn't handle a function call inside a type definition, then it could for a while, now it can't again.
Ha, well I think the pendulum might swing back again on this one at least.
Btw, please do keep these coming but I'm not going to merge them until my latest rewrite is done. From your point of view it shouldn't change too much. No more effects or Data constraint but otherwise similar to the status quo.
