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

Quelle  DependentEvars3.out   Sprache: unbekannt

 
Spracherkennung für: .out vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]


Rocq < 
Rocq < 1 goal
  
  ============================
  (exists n : nat, n = 5 \/ True) /\ (exists m : nat, m = 6 \/ True)

(dependent evars: ; in current goal:)

x < 
x < 2 goals
  
  ============================
  exists n : nat, n = 5 \/ True

goal 2 is:
 exists m : nat, m = 6 \/ True

(dependent evars: ; in current goal:)

x < 2 focused goals (shelved: 1)
  
  ============================
  ?n = 5 \/ True

goal 2 is:
 exists m : nat, m = 6 \/ True

(dependent evars: ?X10:?n; in current goal: ?X10)

x < 2 focused goals (shelved: 1)
  
  ============================
  True

goal 2 is:
 exists m : nat, m = 6 \/ True

(dependent evars: ?X10:?n; in current goal:)

x < 

[ Dauer der Verarbeitung: 0.29 Sekunden  ]