The unifier in the front is not working correctly, at least in part du to the merging of variables and arity-0 schematic functions. Those two played different roles in the unifier before.
The unifier also needs improvement to make it better and more general, see https://github.com/epfl-lara/lisa/issues/34
The interface and documentation may also be improvable.
The unifier in the front is not working correctly, at least in part du to the merging of variables and arity-0 schematic functions. Those two played different roles in the unifier before. The unifier also needs improvement to make it better and more general, see https://github.com/epfl-lara/lisa/issues/34 The interface and documentation may also be improvable.