| products/sources/formale sprachen/Coq/test-suite/ide/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: ssrfwd.mli Sprache: Unknown
|
rahmenlose Ansicht.fake DruckansichtText {Text[95] Latech[113] Fortran[232]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen] # Script simulating a dialog between coqide and coqtop -ideslave # Run it via fake_ide # # Undoing declarations, interleaved with proof steps # new in 8.2 *) # ADD { Theorem k : O=O. } ADD here { assert True by trivial. } ADD { Definition l := O. } ADD { assert True by trivial. } ADD { Definition m := O. } QUERY { Show. } EDIT_AT here # <replay> ADD { Definition l := O. } ADD { assert True by trivial. } ADD { Definition m := O. } # <\replay> ADD { assert True by trivial. } ADD { trivial. } ADD { Qed. } [ Verzeichnis aufwärts0.77unsichere Verbindung ] |