🚀 go-pugleaf

bertrand@eiffel.com (Bertrand Meyer) writes
> I don't really understand the example. How does the system initialize [the
> reference associated with] x: by creation, or by assignment from y?

'x' is initialized by creation. A simple way to look at this is as two
fragments, both involving the same two types.

  A 'V' conforms to a 'U'; V has no 'cp'.

  [1]  x: U;  y: V;     !! x.cp;  x:=y

  [2]  x: U;  y: V;  ! U ! x.cp;  x:=y

As I interpret ETL (in particular p371, the parenthesis in para 6), the two
fragments are semantically identical. [1] is just a shorthand for [2]; since
we know that 'x' is a 'U', the second occurrence of 'U' in [2] is redundant,
and one fragment can be transformed into the other by textual substitution
with no change in semantics.

According to the description of system level validity, however, the two
fragments are different: [2] is valid and [1] is system-invalid.

This strikes me as inconsistent, or at least unreasonable. It seems to me
that "!!" is nothing more than semantic sugar. Why should its use affect
validity?