• Robbert Krebbers's avatar
    Weaken the associativity axiom of the Dra class. · 68ee814e
    Robbert Krebbers authored
    Now, associativity needs only to be established in case the elements are
    valid and their compositions are defined. This is very much like the notion
    of separation algebras I had in my PhD thesis (Def 4.2.1). The Dra to Ra
    construction still easily works out.
sts.v 19 KB