Order specification

Jan 27, 2011 at 8:05 AM

In krml178 page 40 the semantics of orders are specified. It would be nice to include that

 

const a extends b;

is equivalent to a != b && a <: b && ∀x. ((a==x || b==x) <==> ( a<:x && x<:b))


As <: is reflexive, I did not expect the a != b part to be valid.