Skip to content

Add library for monotonic nat ghost state

Tej Chajed requested to merge tchajed/iris-coq:max-nat-ra into master

Implemented as an algebra for rules about auth max_natUR and a logic-level wrapper for the auth element (a nat) and fragment (a persistent lower-bound).

Fixes #327 (closed).

Merge request reports