program_logic.v 737 Bytes
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
(** This file tests a bunch of things. *)
2
From iris.program_logic Require Import model saved_prop.
Ralf Jung's avatar
Ralf Jung committed
3 4

Module ModelTest. (* Make sure we got the notations right. *)
5 6
  Definition iResTest {Λ : language} {Σ : iFunctor}
    (w : iWld Λ Σ) (p : iPst Λ) (g : iGst Λ Σ) : iRes Λ Σ := Res w p g.
Ralf Jung's avatar
Ralf Jung committed
7
End ModelTest.
Ralf Jung's avatar
Ralf Jung committed
8 9 10 11

Module SavedPropTest.
  (* Test if we can really go "crazy higher order" *)
  Section sec.
12
    Definition F : cFunctor := (  -n>  ).
13
    Definition Σ : gFunctors := #[ savedPropGF F ].
Ralf Jung's avatar
Ralf Jung committed
14 15 16
    Context {Λ : language}.
    Notation iProp := (iPropG Λ Σ).

17
    Local Instance : savedPropG Λ Σ F := _.
Ralf Jung's avatar
Ralf Jung committed
18

19
    Definition own_pred γ (φ : iProp -n> iProp) : iProp :=
Ralf Jung's avatar
Ralf Jung committed
20 21 22
      saved_prop_own γ φ.
  End sec.
End SavedPropTest.