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

Quelle  bug_17386.v   Sprache: unbekannt

 
Goal True.
evar (x:nat).
pose (y:=1).
let _ := constr:(eq_refl : x = 1) in idtac.
Show.
(*
x := 1
y := 1

should be
x, y := 1
 *)
Abort.

Messung V0.5
C=87 H=87 G=86

[ Dauer der Verarbeitung: 0.13 Sekunden  (vorverarbeitet)  ]