where n1 ... nx are distinct nominal constants and t does not contain any nominal constant NOT in n1 ... nxor the variable A, has the following solution obtained via eta-contraction:
A = n1\ ... nx\ t.
As an example, the following theorem is provable:
Kind i type.
Theorem foo: forall (E:i -> i -> i) L (F: i -> i), nabla (x y: i),
E y x = L (F x) (F y) -> E = y\x\ L (F x) (F y).
intros. case H1. search.
However, the current implementation of this special case of unification does not distinguish the occurrences of regular constants from those of nominal constants. As a result, the following theorem is NOT provable (which should be):
Type arrow i -> i -> i.
Theorem bug: forall E (L:i -> i), nabla (x y: i),
E y x = L (arrow x y) -> E = y\x\ L (arrow x y).
intros. case H1. (* stuck *)
Abllea incorrectly assumes that arrow should be a nominal constant occuring in [y, x] for the unification to be possible.
The following unification problem
where
n1 ... nxare distinct nominal constants andtdoes not contain any nominal constant NOT inn1 ... nxor the variableA, has the following solution obtained via eta-contraction:As an example, the following theorem is provable:
However, the current implementation of this special case of unification does not distinguish the occurrences of regular constants from those of nominal constants. As a result, the following theorem is NOT provable (which should be):
Abllea incorrectly assumes that
arrowshould be a nominal constant occuring in[y, x]for the unification to be possible.