Hello! Do you know if anti-unification is used in the implementation of Coq? It seems to be used in Agda (https://github.com/UlfNorell/agda/commit/7c8bc3b40503b7efba55f96225ad8ea71942aa85), but I am not sure why.
Last updated: Oct 13 2024 at 01:02 UTC