PML can not always use function equalities that it learned

[craff]

When we learn that functions are equal, we should keep that information:
VN_LAbs should contain a list of functions.

This would allow to always deduce f x = g x from f = g

[rlepigre]

I don't understand why this would be required. If f = g, then it is immediate that f x = g x.

[craff]

Assume PML learns f = g prior to the creation of the term "f x", without loss of generality, let us assume that f points to g in the union find map. Then, forming the term "f x" (or "g x"), we will only compute "g x".

In PML one, abstraction nodes were carying a list of functions, just to compute both f x and g x and call "union" on the result.

[craff]

Mais, bon, on n'a pas d'exemple encore avec des hypothèses de la forme f = g, où f et g ne sont pas des variables ... Donc ça peut attendre.

[rlepigre]

OK, cool, j'avais pas pensé à ça !