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 441 B image not shown  

Quelle  join-module2.fake   Sprache: unbekannt

 
# Script simulating a dialog between rocqide and coqtop -ideslave
# Run it via fake_ide
#
# Failing join from within a module
#

ADD { Universes u v. }
ADD { Lemma foo : True. }
ADD { Proof. }
ADD { refine (let _ : Type@{v} := Type@{u} in _). }
ADD { constructor. }
ADD { Qed. }
ADD { Lemma bar : True. }
ADD { Proof. }
ADD { refine (let _ : Type@{u} := Type@{v} in _). }
ADD { constructor. }
ADD { Qed. }
ADD { Module Foo. }
FAILJOIN
ABORT

[ Dauer der Verarbeitung: 0.14 Sekunden  (vorverarbeitet)  ]