cic-redex

cic-redex copied to clipboard

The current attempt at getting an algorithmic conversion rule isn't quite right, as it doesn't allow for transitive subtyping. E.g. if `A` reduces to `B`, and `B` is a subtype...

wilbowma

I don't seem to have any tests with indexed types.

wilbowma

While I think they implement the same logic, the rule is a little too far from the spec, and not necessarily so.

wilbowma