| products/Sources/formale Sprachen/Coq/test-suite/ide/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: simpdata.ML Sprache: Coq
|
Spracherkennung für: .fake vermutete Sprache: Text {Text[77] Latech[78] Fortran[253]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen] # Script simulating a dialog between coqide and coqtop -ideslave # Run it via fake_ide # # focusing a broken proof and fixing it # first proof ADD { Lemma a : True. } ADD { Proof using. } ADD here { idtac. } ADD { exact Ix. } ADD { Qed. } # second proof ADD { Lemma b : False. } ADD { Proof using. } ADD { give_up. } ADD last { Admitted. } # We join and expect some proof to fail WAIT # Going back to the error EDIT_AT here # Fixing the proof ADD { exact I. } ADD { Qed. } # we are back at the end ASSERT TIP last QUERY { Check a. } QUERY { Check b. } [ Dauer der Verarbeitung: 0.160 Sekunden ] |