Open 7h3kk1d opened 1 week ago
what happens with alpha equivalent types (e.g. forall x -> (x, x)
and forall a -> (a, a)
)?
what happens with alpha equivalent types (e.g.
forall x -> (x, x)
andforall a -> (a, a)
)?
@cyrus- According to the docstring it should do alpha equivalence but not normalization. https://github.com/hazelgrove/hazel/blob/dev/src/haz3lcore/statics/TermBase.re#L693
If we don't want it for alpha equivalent types I can introduce a 3rd form of equality that just ignores IDs.
This may be a bug somewhere else as well though
Old version New version
Depends on https://github.com/hazelgrove/hazel/pull/1409 for a notion of ID-unaware equality.