tests.v 743 Bytes
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
(** This file tests a bunch of things. *)
Ralf Jung's avatar
Ralf Jung committed
2
From 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
  Definition iResTest {Λ : language} {Σ : rFunctor}
6
    (w : iWld Λ Σ) (p : iPst Λ) (g : iGst Λ Σ) : iRes Λ Σ := Res w p (Some g).
Ralf Jung's avatar
Ralf Jung committed
7
End ModelTest.
Ralf Jung's avatar
Ralf Jung committed
8
9
10
11
12
13
14
15
16
17
18
19
20
21

Module SavedPropTest.
  (* Test if we can really go "crazy higher order" *)
  Section sec.
    Definition Σ : rFunctorG := #[ agreeRF (cofe_morCF idCF idCF) ].
    Context {Λ : language}.
    Notation iProp := (iPropG Λ Σ).

    Local Instance : savedPropG Λ Σ (cofe_morCF idCF idCF) := _.

    Definition own_pred γ (φ : laterC iProp -n> laterC iProp) : iProp :=
      saved_prop_own γ φ.
  End sec.
End SavedPropTest.