Tactic.failIfNotDecided constructor

Tactic.failIfNotDecided(
  1. Context c
)

Creates a tactic that always fails if the given goal is not trivially decidable.

Implementation

factory Tactic.failIfNotDecided(Context c) {
  final result = c._z3.tactic_fail_if_not_decided();
  return c._getTactic(result);
}