Strings are inhabited

See merge request iris/stdpp!70

Fix typo in instance name

See merge request iris/stdpp!69

Now we follow Coq's stdlib and declare this instance using a `Hint Extern`;
this avoids making `flip` type class opaque.

Revert "`RelDecision` instance for `flip`, and make `flip` tc opaque to avoid loops due to eager unification."

This reverts commit b81aa3aa.

`RelDecision` instance for `flip`, and make `flip` tc opaque to avoid loops due to eager unification.

Otherwise type class search ocasionally unfolds them and finds
wrong instances. Based on an issue reported by @jihgfee.

Fix typo in doc

See merge request iris/stdpp!68

Binders library that's used in many Iris developments.

See merge request iris/stdpp!67

This closes issue #25.

Improve performance of `set_solver`

Closes #29 and iris#232

See merge request !66

gmultiset lemmas

See merge request iris/stdpp!65

Add `map_delete_zip_with`

See merge request iris/stdpp!64

More efficient list encoding for Countable

See merge request !62

Jakob Botsch Nielsen authored 6 years ago and Robbert Krebbers committed 6 years ago

This changes the encoding used for finite lists of values of countable
types to be linear instead of exponential. The encoding works by
duplicating bits of each element so that 0 -> 00 and 1 -> 11, and then
separating each element with 10. The top 1-bits are not kept since we
know a 10 is starting a new element which ends with a 1.

Fix #28

Hopefully this fixes iris#232