Removed involutive file

parent 80b8d626
-Q theories osiris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/typing/involutive.v
theories/typing/side.v
theories/typing/stype.v
theories/encodings/encodable.v
......
......@@ -206,7 +206,7 @@ Section stype.
by iRewrite "Heq" in "Heval".
- iRewrite "Heq" in "Heval". destruct r as [|vr r]=> //=.
iSplit; first done.
iRewrite "Heval". simpl. iFrame "HP". by rewrite involutive. }
iRewrite "Heval". simpl. iFrame "HP". by rewrite dual_stype_involutive. }
iModIntro. iFrame. auto.
- iExists _.
iIntros "{$Hcrf} !>" (v) "HP Hcrf".
......@@ -220,7 +220,7 @@ Section stype.
iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
- iRewrite "Heq" in "Heval". destruct l as [|vl l]=> //.
iSplit; first done. simpl.
iRewrite "Heval". simpl. iFrame "HP". by rewrite involutive.
iRewrite "Heval". simpl. iFrame "HP". by rewrite dual_stype_involutive.
- iSplit=> //.
iApply (st_eval_send with "HP").
by iRewrite "Heq" in "Heval". }
......
From iris.heap_lang Require Import proofmode notation.
Class Involutive {A} (R : relation A) (f : A A) :=
involutive x : R (f (f x)) x.
\ No newline at end of file
......@@ -4,9 +4,11 @@ From stdpp Require Export list.
From iris.base_logic Require Import base_logic.
From iris.algebra Require Import updates local_updates.
From iris.heap_lang Require Import proofmode notation.
From osiris.typing Require Import involutive.
Set Default Proof Using "Type".
Class Involutive {A} (R : relation A) (f : A A) :=
involutive x : R (f (f x)) x.
Inductive action := Send | Receive.
Instance action_inhabited : Inhabited action := populate Send.
Definition dual_action (a : action) : action :=
......
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