Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
1 result
Blame Permalink
Forked from Iris / Iris
5043 commits behind the upstream repository.
  • Robbert Krebbers's avatar
    68ee814e
    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.
    68ee814e
    History
    Weaken the associativity axiom of the Dra class.
    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.
dra.v 9.39 KiB