heap_lang2.v 619 Bytes
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.
4
From iris.heap_lang Require Export lifting notation.
5 6 7 8
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".

Section printing_tests.
9
  Context `{!heapG Σ}.
10 11 12 13 14 15 16 17 18 19 20

  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.

End printing_tests.