plausible is strictly better than sorry – it will only complain if it finds a concrete counter-example, and otherwise will let proofs go through. We could rename --allow-sorry to --allow-plausible.
When --allow-plausible is not given, we may still want to add plausible as the last tactic step if all previous steps fail. Instead of opaque errors about unsolved goals, this may sometimes generate a concrete counter-example, which would be more helpful to users.
plausibleis strictly better thansorry– it will only complain if it finds a concrete counter-example, and otherwise will let proofs go through. We could rename--allow-sorryto--allow-plausible.When
--allow-plausibleis not given, we may still want to addplausibleas the last tactic step if all previous steps fail. Instead of opaque errors about unsolved goals, this may sometimes generate a concrete counter-example, which would be more helpful to users.