-
Gabriel Scherer authored
A typed hole can have any type (it imposes no typing constraints on the context around it), and its subterms can have any type (the hole imposes no constraint on them). This is the ultimate language construct to do type-preserving shrinking. When shrinking it is important to be able to remove subterms that do not participate to the error. Holes with no subterms can be used to completely erase a term, as implemented in this commeit. Holes with subterms can be used to selectively erase parts of a term (for example, the application "t u" can be rewritten into the hole "...[t, u]", erasing only the application rule), but this is not implemented yet in the present commit.
2ac0c429