Alan Manuel Gloria:
> Looks pretty good, although I'm kind of confused in your ACL2 example
> - is the syntax for nonpunctuation infix {x implies b} or {a /implies/
> b}? Or does {} automatically assume that if the second entry in a
> 3-entry list is a symbol (regardless of punctuation or lack thereof)
> it must be infix (for non-infixed default)?
Well, there's an excellent reason that you're confused about that example: I
made a cut-and-paste error. Sorry about that! I _think_ I've fixed it.
The ACL2 example is probably important because it's one of the few times where
infix-default has a specific advantage (you can have a spelled-out infix
operator WITHOUT disabling indentation). But on looking at it, it's not a
compelling example.
I was surprised how often the "infix default" and "infix non-default" ended up
being the same, or nearly so. All the extra rule complexity just doesn't seem
to be as helpful as I expected.
> > 6. Immediate completion. A single complete expression that begins at the
> > left edge of a line, and is immediately followed by newline after it
> > completes, causes the expression to immediately complete... Type an initial
> > space if you want to enter only a single complete expression on a line yet
> > follow it with child lines.
>
> Hmm, this seems to conflict with your BitC example:
> deftypeclass
> forall (Eql('a)) Ord('a)
> < : fn(('a 'a) 'a)
> So: does deftypeclass have a starting space or no? And why not?
Yes, it DOES have a starting space. So no problem... at least conceptually.
> Hmm, come to think of it this rule is kinda confusing to me...
Understand. Actually, the indentation stuff has some serious problems as I
examine it more closely. The Scheme spec for indentation hides some really
serious problems - I don't think it got enough serious use before they spec'ed
it.
I think that entire rule "starting space" etc. rule will have to go away. But
I think that's better left for a separate thread of emails - the problem is
subtle. I'd really like the guy who developed I-expressions to be involved, if
I can get him.
--- David A. Wheeler
