Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Roqc/test-suite/ide/   (Beweissystem des Inria Version 9.1.0©)  Datei vom 15.8.2025 mit Größe 317 B image not shown  

Quelle  undo002.fake   Sprache: unbekannt

 
# Script simulating a dialog between rocqide and coqtop -ideslave
# Run it via fake_ide
#
# Simple backtrack by 2 before two global definitions
#
ADD initial { Comments "initial sentence". }
ADD { Definition foo := 0. }
ADD { Definition bar := 1. }
EDIT_AT initial
QUERY { Fail Check foo. }
QUERY { Fail Check bar. }

[ Dauer der Verarbeitung: 0.3 Sekunden  (vorverarbeitet)  ]