Skip to content

2.1.0

Choose a tag to compare

@aleksnanevski aleksnanevski released this 16 Jan 12:41
· 17 commits to master since this release
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.