Marc Weber wrote:
Excerpts from Adam Chlipala's message of Tue Dec 21 00:42:14 +0100 2010:
Marc Weber wrote:
In which way is this related to the
e! guarded expression application?
The points where these need to be inserted are usually inferred.
The demos make use of it multiple times:
[...]
Or do those ! have a different meaning?
Each of these should be an application of something besides an
identifier defined at the top level of a module.
I've tried adding the ! everywhere at the examples you posted. But nothing
compiled.
If the program compiles without it, adding it will always break things.
You have to prefix a module top-level identifier with [...@] at a call site
to make disjointness obligations explicit.
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
