products/sources/formale sprachen/Coq/test-suite/ide/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: SeqSeries.v   Sprache: Coq

Untersuchungsergebnis.fake Download desLatech {Latech[64] Isabelle[243] Fortran[248]}zum Wurzelverzeichnis wechseln

# Script simulating a dialog between coqide and coqtop -ideslave
# Run it via fake_ide
#
# jumping between broken proofs + interp error while fixing.
# the error should note make the GUI unfocus the currently focused proof.
 
# first proof
ADD { Lemma a : True. }
ADD here { Proof using. }
ADD { fail. }
ADD { trivial. } # first error
ADD { Qed. }
WAIT
EDIT_AT here
# Fixing the proof
ADD fix { trivial. }
ADD { Qed. }
WAIT
EDIT_AT fix
ADD { Qed. }
JOIN

[ zur Elbe Produktseite wechseln0.80Quellennavigators  ]