Skip to content

2.1.0

Latest
Compare
Choose a tag to compare
@aleksnanevski aleksnanevski released this 16 Jan 12:41
a0b2563
  • A new minor release to support Hierarchy Builder 1.8.
  • Added automation for reasoning about uniqueness of sequences.
  • Added a type class of conical PCMs.
  • Made dom infer the union_map structure, in order to support structure-specific notation for dom.
  • Added a type class of total map-like functions in unionmap.v. Previous version had only partial map-like function (omap_fun), but total ones admit better lemmas.
  • Generalized several \big lemmas in unionmap.v that were previously unnecessarily restricted (bigD1FE, bigPtUnE, bigPtUn, bigDUE).
  • Added a number of smaller lemmas in pred, prelude, seqext, unionmap.