guard_hyp

Tactic to check that a named hypothesis has a given type and/or value.

• guard_hyp h : t checks the type up to reducible defeq,

• guard_hyp h :~ t checks the type up to default defeq,

• guard_hyp h :ₛ t checks the type up to syntactic equality,

• guard_hyp h :ₐ t checks the type up to alpha equality.

• guard_hyp h := v checks value up to reducible defeq,

• guard_hyp h :=~ v checks value up to default defeq,

• guard_hyp h :=ₛ v checks value up to syntactic equality,

• guard_hyp h :=ₐ v checks the value up to alpha equality.

The value v is elaborated using the type of h as the expected type.

guard_target

Tactic to check that the target agrees with a given expression.

• guard_target = e checks that the target is defeq at reducible transparency to e.

• guard_target =~ e checks that the target is defeq at default transparency to e.

• guard_target =ₛ e checks that the target is syntactically equal to e.

• guard_target =ₐ e checks that the target is alpha-equivalent to e.

The term e is elaborated with the type of the goal as the expected type, which is mostly useful within conv mode.

guard_expr

Tactic to check equality of two expressions.

• guard_expr e = e' checks that e and e' are defeq at reducible transparency.

• guard_expr e =~ e' checks that e and e' are defeq at default transparency.

• guard_expr e =ₛ e' checks that e and e' are syntactically equal.

• guard_expr e =ₐ e' checks that e and e' are alpha-equivalent.

Both e and e' are elaborated then have their metavariables instantiated before the equality check. Their types are unified (using isDefEqGuarded) before synthetic metavariables are processed, which helps with default instance handling.

fail_if_success

fail_if_success t fails if the tactic t succeeds.