heap_lang2.v 1.01 KB
Newer Older
1
2
3
(* Test yet another way of importing heap_lang modules that used to break
printing *)
From iris.proofmode Require Import tactics.
Ralf Jung's avatar
Ralf Jung committed
4
From iris.heap_lang Require Export primitive_laws notation.
5
6
7
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".

8
9
Unset Mangle Names.

10
Section printing_tests.
11
  Context `{!heapG Σ}.
12

13
14
15
16
  Lemma vs_print (P Q : iProp Σ) :
    P ={}= Q.
  Proof. Show. Abort.

17
18
19
20
21
22
23
24
25
  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) :
    True - WP let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"  {{ _, True }}.
  Proof.
    iIntros "_". Show.
  Abort.

26
27
28
29
30
31
32
33
34
  Lemma texan_triple_long_expr (fun1 fun2 fun3 : expr) :
    {{{ True }}}
       let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"
    {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
  Proof. Show. Abort.

35
End printing_tests.