Spracherkennung für: .out vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
Rocq < Rocq < Toplevel input, characters 7-9:
> Check $x.
> ^^
Error: Unbound value x
Rocq < Rocq < Toplevel input, characters 16-17:
> Check $preterm:x.
> ^
Error: Unbound value x
Rocq < Rocq < Toplevel input, characters 7-8:
> Check $ x.
> ^
Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]).
Rocq < Rocq < Toplevel input, characters 7-8:
> Check $ preterm:x.
> ^
Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]).
Rocq < Rocq < Toplevel input, characters 7-8:
> Check $ preterm : x.
> ^
Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]).
Rocq < Rocq < Toplevel input, characters 18-19:
> Check $preterm : x.
> ^
Error: The reference x was not found in the current environment.
Rocq < Rocq < Toplevel input, characters 16-24:
> Check fun x => $preterm : x.
> ^^^^^^^^
Error: Unbound value preterm
Rocq < Rocq < Toplevel input, characters 17-18:
> Check $preterm: x.
> ^
Error: The reference x was not found in the current environment.
Rocq < Rocq < Toplevel input, characters 16-24:
> Check fun x => $preterm: x.
> ^^^^^^^^
Error: Unbound value preterm
Rocq < Rocq < Toplevel input, characters 7-8:
> Check $ preterm :x.
> ^
Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]).
Rocq <
[ Dauer der Verarbeitung: 0.31 Sekunden
]
