Skip to content
GitLab
Explore
Sign in
Iris
Iris
Repository
iris
lib
ModuRes
MetricCore.v
Find file
Blame
History
Permalink
make it possible to state contractiveness for any function (not just non-expansive ones).
· a65a59a8
Ralf Jung
authored
Feb 19, 2015
This gets rid of an unnecessary proof obligation for wpF.
a65a59a8