| products/sources/formale sprachen/Coq/test-suite/ide/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: intros.v Sprache: Unknown
|
Untersuchungsergebnis.fake Download desText {Text[78] Latech[108] Fortran[246]}zum Wurzelverzeichnis wechseln # Script simulating a dialog between coqide and coqtop -ideslave # Run it via fake_ide # # Undoing declarations, interleaved with proof steps and commands *) # new in 8.2 *) # ADD { Theorem n : O=O. } ADD s2 { assert True by trivial. } ADD s3 { Definition o := O. } ADD s4 { Ltac h x := x. } ADD s5 { assert True by trivial. } ADD s6 { Focus. } ADD { Definition p := O. } EDIT_AT s6 EDIT_AT s5 EDIT_AT s4 EDIT_AT s3 EDIT_AT s2 # <replay> ADD { Definition o := O. } ADD { Ltac h x := x. } ADD { assert True by trivial. } ADD { Focus. } ADD { Definition p := O. } # </replay> ADD { assert True by trivial. } ADD { trivial. } ADD { Qed. } [ zur Elbe Produktseite wechseln0.73Quellennavigators ] |