[Ur] simple example about constructing rects - guarded types?

[Adam Chlipala]

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.