Commit 8a675a00 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove old tests about heap_lang reductions.

parent aeff566c
......@@ -5,19 +5,6 @@ From iris.heap_lang Require Import adequacy.
From iris.program_logic Require Import ownership.
From iris.heap_lang Require Import proofmode notation.
(* FIXME or remove
Section LangTests.
Definition add : expr := #21 + #21.
Goal ∀ σ, head_step add σ (#42) σ [].
Proof. intros; do_head_step done. Qed.
Definition rec_app : expr := (rec: "f" "x" := "f" "x") #0.
Goal ∀ σ, head_step rec_app σ rec_app σ [].
Proof. intros. rewrite /rec_app. do_head_step done. Qed.
Definition lam : expr := λ: "x", "x" + #21.
Goal ∀ σ, head_step (lam #21)%E σ add σ [].
Proof. intros. rewrite /lam. do_head_step done. Qed.
End LangTests. *)
Section LiftingTests.
Context `{heapG Σ}.
Implicit Types P Q : iProp Σ.
Supports Markdown
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