Forked from
Iris / stdpp
2413 commits behind the upstream repository.
Robbert Krebbers
authored
Using this new definition we can express being contractive using a Proper. This has the following advantages: - It makes it easier to state that a function with multiple arguments is contractive (in all or some arguments). - A solve_contractive tactic can be implemented by extending the solve_proper tactic.
Name | Last commit | Last update |
---|---|---|
theories |