All have and pose forms in proofs are recorded as local and transparent (and parameter-less) definitions.
This can make the normalization process quite long since the same definition can be normalized a large number
of times... One way to circumvent this problem would be to implement a normalization cache.
This should be benchmarked first.
All
haveandposeforms in proofs are recorded as local and transparent (and parameter-less) definitions. This can make the normalization process quite long since the same definition can be normalized a large number of times... One way to circumvent this problem would be to implement a normalization cache. This should be benchmarked first.