VALID_LT

Tactical.VALID_LT : list_tactic -> list_tactic

Makes a list-tactic fail if it would otherwise return an invalid proof.

When list-tactic ltac is applied to a goal list gl it produces a new goal list gl' and a justification. When the justification is applied to a list thl' of theorems which are the new goals gl', proved, it should produce a list thl of theorems which are the goals gl, proved.

Precisely, for each goal (asl, g) in gl, the corresponding theorem in thl should be A |- g, with A a subset of asl. If this is not the case, then the list-tactic is invalid, and VALID_LT ltac gl fails (raises an exception). Otherwise, VALID_LT ltac gl behaves the same as ltac gl.

Failure

VALID_LT ltac gl fails by design if ltac gl produces new goals and justification which do not prove the given goals gl. Also fails if its ltac gl fails.

See also

Tactical.VALID, Tactical.VALIDATE_LT, proofManagerLib.elt, proofManagerLib.expand_list