Hanno Becker (Dec 29 2022 at 09:06): Hanno Becker (Dec 29 2022 at 09:06):Hi! I'm using Eisbach's match to perform a top-level pattern matching on a conclusion and pass part of the match result to a lower level tactic which _also_ performs pattern matching to identify suitable simplification operations. The initial conclusion has schematic variables, but they seem to have been lost by the time the low-level tactic is invoked. Does match remove schematics?
Last updated: Dec 28 2025 at 02:03 UTC