- Mar 14, 2019
-
-
Robbert Krebbers authored
move the (very brief) contribution guide to the README See merge request iris/stdpp!60
-
Ralf Jung authored
-
Robbert Krebbers authored
Make `gset` a `Definition` instead of `Notation`. See merge request iris/stdpp!59
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Mar 06, 2019
-
-
Robbert Krebbers authored
-
- Mar 04, 2019
-
-
Robbert Krebbers authored
This fixes an issue in orc11.
-
- Mar 03, 2019
-
-
Robbert Krebbers authored
Overhaul of the `Infinite`/`Fresh` infrastructure See merge request iris/stdpp!58
-
Robbert Krebbers authored
-
Robbert Krebbers authored
- The class `Infinite A` is now defined as having a function `fresh : list A → A`, that given a list `xs`, gives an element `x ∉ xs`. - For most types this `fresh` function has a sensible computable behavior, for example: + For numbers, it yields one added to the maximal element in `xs`. + For strings, it yields the first string representation of a number that is not in `xs`. - For any type `C` of finite sets with elements of infinite type `A`, we lift the fresh function to `C → A`. As a consequence: - It is now possible to pick fresh elements from _any_ finite set and from _any_ list with elements of an infinite type. Before it was only possible for specific finite sets, e.g. `gset`, `pset`, ... - It makes the code more uniform. There was a lot of overlap between having a `Fresh` and an `Infinite` instance. This got unified.
-
- Mar 01, 2019
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Feb 28, 2019
- Feb 23, 2019
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- Feb 22, 2019
-
-
Ralf Jung authored
-
- Feb 21, 2019
-
-
Robbert Krebbers authored
Notion of (in)finite predicates See merge request iris/stdpp!56
-
Robbert Krebbers authored
Additionally lemmas for insert, nth, take, and list_find See merge request iris/stdpp!55
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Rename multiset "union" into "disjoint union" Closes #13 See merge request iris/stdpp!57
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Also, use the union name/class/symbol for what's usually the union, and define the intersection on multisets.
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- Feb 20, 2019
-
-
Ralf Jung authored
fix or silence Coq 8.10 warnings See merge request iris/stdpp!52
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
New `seq` operation on maps + consistency tweaks for `seq` operation on sets See merge request iris/stdpp!44
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-