Example in 2.5 doesn't follow the definition of size in 2.2

[marklemay]

1 + |e| + |Const(7)| = 8 + |e|

should be

1 + |e| + 1 = 8 + |e|

not

1 + |e| + 7 = 8 + |e|

Assuming | | represents the same size operation defined in 2.2

[cpitclaudel]

And that 8 should be a 2

[achlipala]

Thanks; fixed!