Re: [isabelle] HOL parser question



On Tue, 13 Mar 2007, Christian Maeder wrote:

>  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>"
> 
> Why this, is the name space for types and constants not separated?

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.