Commit 14821493 authored by Daniel Gratzer's avatar Daniel Gratzer

Restore comments

parent 9f47522f
Pipeline #15264 failed with stage
......@@ -4,6 +4,8 @@ From iris.heap_lang Require Import notation proofmode.
From iris_examples.concurrent_stacks Require Import specs.
Set Default Proof Using "Type".
(** Stack 1: No helping, bag spec. *)
Definition new_stack : val := λ: "_", ref NONEV.
Definition push : val :=
rec: "push" "s" "v" :=
......
......@@ -5,6 +5,8 @@ From iris.program_logic Require Export weakestpre.
From iris_examples.concurrent_stacks Require Import specs.
Set Default Proof Using "Type".
(** Stack 2: Helping, bag spec. *)
Definition mk_offer : val :=
λ: "v", ("v", ref #0).
Definition revoke_offer : val :=
......
......@@ -3,6 +3,8 @@ From iris.heap_lang Require Export lang proofmode notation.
From iris_examples.concurrent_stacks Require Import specs.
Set Default Proof Using "Type".
(** Stack 3: No helping, CAP spec. *)
Definition mk_stack : val := λ: "_", ref NONEV.
Definition push : val :=
rec: "push" "s" "v" :=
......
......@@ -3,6 +3,8 @@ From iris.heap_lang Require Export lang proofmode notation.
From iris.algebra Require Import excl.
From iris_examples.concurrent_stacks Require Import specs.
(** Stack 4: Helping, CAP spec. *)
Definition mk_offer : val :=
λ: "v", ("v", ref #0).
Definition revoke_offer : val :=
......
Markdown is supported
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