Commit 56f0afb2 authored by Ralf Jung's avatar Ralf Jung

provide functor for cancellable invariants

parent e5bb24e7
......@@ -5,6 +5,10 @@ Set Default Proof Using "Type".
Import uPred.
Class cinvG Σ := cinv_inG :> inG Σ fracR.
Definition cinvΣ : gFunctors := #[GFunctor fracR].
Instance subG_cinvΣ {Σ} : subG cinvΣ Σ cinvG Σ.
Proof. solve_inG. Qed.
Section defs.
Context `{invG Σ, cinvG Σ}.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment