Zgodnie z taktyką, taktyka destruct ma wariant akceptujący "łączący rozłączny wzór wprowadzający", który umożliwia użytkownikowi przypisywanie nazw wprowadzanych zmiennych, nawet podczas rozpakowywani
Podczas implementacji złożonej taktyki w Ltacu, istnieje kilka poleceń Ltac lub taktyki, które oczekują na niepowodzenie i gdzie jest to oczekiwane (na przykład zakończenie repeat lub spowodowanie cof
Próbuję napisać regułę dla hipotez, skomponowany z pomocą match budowy: Goal forall x:nat, (match x with | 1 => 5 | _ => 10 end = 5 -> x = 1)%nat.
intros.
x : nat
H : match x with
| 0%nat =>