Stream: General

Topic: Schematics in Eisbach

view this post on Zulip 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 07 2023 at 08:19 UTC