Demo: 'data', 'idata' syntax: stick the quote in

[GoogleCodeExporter]

We currently write:

data Bool := (false : Bool) ; (true : Bool) ;

elab 'true : Bool ;
elab 'false : Bool ;

The spectators are confused by the fact that we write "false" in the data 
declaration, while we use "'false" everywhere else.

Original issue reported on code.google.com by pedag...@gmail.com on 7 Sep 2010 at 9:35

[GoogleCodeExporter]

I think the spectators are right. We need to be clear about the distinction 
between tags and identifiers, both in our syntax and in the way we talk and 
write.

People used to ML or Haskell (or even to Agda) will expect constructors to be a 
special kind of identifier, with scope and type. Our tags have no inherent 
scope or type. I guess we need to explain the bidirectional deal.

We do need some way to distinguish the tags from the identifiers. The quote is 
a bit ugly, but it fulfils that need, for the time being.

Original comment by co...@strictlypositive.org on 8 Sep 2010 at 10:38

• Added labels: ****
• Removed labels: ****

[GoogleCodeExporter]

Fixed by "(I)Data: constructor definitions takes a quote mark (for uniformity)".

Original comment by pedag...@gmail.com on 8 Sep 2010 at 11:09

• Changed state: Fixed
• Added labels: ****
• Removed labels: ****