| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/success/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 310 B |
|
Quelle TacticNotation2.v Sprache: Coq |
|||||||||||||||
|
Tactic Notation "complete" tactic(tac) := tac; fail. Ltac f0 := complete (intuition idtac). (** FIXME: This is badly printed because of bug #3079. At least we check that it does not fail anomalously. *) Print Ltac f0. Ltac f1 := complete f1. Print Ltac f1. Ltac f2 := complete intuition. Print Ltac f2.
¤ Dauer der Verarbeitung: 0.3 Sekunden ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-04-02