| products/sources/formale sprachen/Coq/test-suite/ide/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: Ranalysis1.v Sprache: Coq
|
Untersuchungsergebnis.fake Download desLatech {Latech[97] Fortran[206] Ada[250]}zum Wurzelverzeichnis wechseln # Script simulating a dialog between coqide and coqtop -ideslave # Run it via fake_ide # # Test backtracking in presence of nested proofs # Second, trigger the undo of an inner proof # ADD { Set Nested Proofs Allowed. } ADD { Lemma aa : True -> True /\ True. } ADD { intro H. } ADD { split. } ADD { Lemma bb : False -> False. } ADD { intro H. } ADD { apply H. } ADD { Qed. } ADD { apply H. } ADD { Lemma cc : False -> True. } ADD { intro H. } ADD here { destruct H. } ADD { Qed. } ADD { apply H. } EDIT_AT here # <replay> ADD { Qed. } ADD { apply H. } # </replay> ADD { Qed. } QUERY { Fail Show. } QUERY { Check (aa,bb,cc). } [ zur Elbe Produktseite wechseln0.93Quellennavigators ] |