Spracherkennung für: .out vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
Rocq < Rocq < 1 goal
============================
True
Unnamed_thm <
Unnamed_thm < Unnamed_thm < Unnamed_thm < Toplevel input, characters 111-112:
> | match goal with x := ?v |- _ => exact v end].
> ^
Error:
In environment
x := Top.Unnamed_thm_subproof : nat
The term "Top.Unnamed_thm_subproof" has type "nat"
while it is expected to have type "True".
Unnamed_thm <
[Dauer der Verarbeitung: 0.18 Sekunden, vorverarbeitet 2026-06-04]
