• Robbert Krebbers's avatar
    Miscellaneous changes to the memory · ab930b45
    Robbert Krebbers authored
    * Remove generic path_typed instance for lists. For the zippers in the
      operational semantics, it goes the other way around.
    * Remove constructor lemmas for values/memory_trees and use a generic tactic
      instead. This tactic uses the standard constructor tactic, but folds the
      type classes afterward.
    ab930b45
list.v 140 KB