Email Gateway (Aug 18 2022 at 10:19): Email Gateway (Aug 18 2022 at 10:19):From: Christian Maeder <maeder@tzi.de>
Hi,
for
datatype A = c ("A")
datatype B = B A
I get the following parser error:
*** Inner syntax error at: "A"
*** Expected tokens: "_" "(" "[" "tvar" "tid" "longid" "id" "(|" "\<lparr>"
*** The error(s) above occurred in type "A"
*** The error above occured in constructor B of datatype B
*** At command "datatype".
however,
datatype A = A
datatype B = B A
or,
datatype A = A ("c")
datatype B = B A
is accepted.
Why this, is the name space for types and constants not separated?
Cheers Christian
D.thy
Email Gateway (Aug 18 2022 at 10:19):From: Makarius <makarius@sketis.net>
The name spaces are separate, but not the token space for concrete syntax.
Using "A" as a literal rules out any further use elsewise.
Makarius
Last updated: May 03 2024 at 08:18 UTC