Anyone know a reliable way to get an unsolvable delayed constraint from a tactic? so eg tac; gfail. would say "tactic failure" but tac. would error in the implicit constraint solving
tac; gfail.
tac.
Last updated: Oct 13 2024 at 01:02 UTC