• Robbert Krebbers's avatar
    Many STS tweaks: · 9997d0ef
    Robbert Krebbers authored
    * Clearly separate the file algebra/sts in three parts:
      1.) The definition of an STS, step relations, and closure stuff
      2.) The construction as a disjoint RA (this module should never be used)
      3.) The construction as a CMRA with many derived properties
    * Turn stsT into a canonical structure so that we can make more of its arguments
      implicit.
    * Rename the underlying step relation of STSs to prim_step (similar naming as
      for languages, but here in a module to avoid ambiguity)
    * Refactor program_logic/sts by moving general properties of the STS CMRA to
      algebra/sts.v
    * Make naming and use of modules in program_logic/sts more consistent with
      program_logic/auth and program_logic/saved_prop
    * Prove setoid properties of all definitions in program_logic/sts
    9997d0ef
dra.v 6.2 KB