BLD equality/named arguments tie-up problem

The way the semantics is defined for BLD implies that there are implicit
equalities such as  p(a->b c->d) = p(c->d a->b).
So, even if the head-equality, which is at risk, is taken out, BLD will still
have am infinite number of axiomatic equality facts (= head equalities).

I think it is desirable to avoid this tie-up and change the semantics. This
would affect both BLD and FLD, but not Core.

Not sure whether this can pass as an insubstantial change or not.

michael

Received on Saturday, 19 December 2009 07:52:43 UTC