|
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.16 Sekunden
(vorverarbeitet)
]
|
