HOL
HOL copied to clipboard
HOL-Theorem-Prover
Use an efficient datastructure for substitution
Currently, functions like match_term return substitutions represented as a list of pairs. Why don't all these functions use maps instead of lists?
Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.
Historical reasons, mainly. Do you have an application needing a huge number of substitutions?
Konrad.
On Fri, Apr 8, 2016 at 9:46 PM, Jack Gallagher [email protected] wrote:
Currently, functions like match_term return substitutions represented as a list of pairs. Why don't all these functions use maps instead of lists?
— You are receiving this because you are subscribed to this thread. Reply to this email directly or view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/336
Probably not - needed to use them when writing match_goal and was curious why they worked that way. Substitution lists coming from that should mostly be short (though if people start writing tactics with it that get run 1000+ times in a loop a more cache friendly structure might make a difference)