The current implementation of split forall relies on a partial copy of expand head, this is done because currently expand head is not parametrized over the substitutions.
Here instead I extend Substs with a capture function that allows split forall to be done with expand head and the substitutions captured. This approach will likely be used also on Check in the future.
Goals
Faster and more solid code.
Context
The current implementation of split forall relies on a partial copy of expand head, this is done because currently expand head is not parametrized over the substitutions.
Here instead I extend
Substswith a capture function that allows split forall to be done with expand head and the substitutions captured. This approach will likely be used also on Check in the future.Related
199