diff --git a/tests/one_shot.v b/tests/one_shot.v index 01159f1a77a05459cdbb1acd0a4d7f9999bf6755..dd9f08ed060ab562e79a19aee1753fe845ea1dea 100644 --- a/tests/one_shot.v +++ b/tests/one_shot.v @@ -6,6 +6,9 @@ From iris.proofmode Require Import tactics. From iris.heap_lang.lib Require Import par. Set Default Proof Using "Type". +(** This is the introductory example from the "Iris from the Ground Up" journal +paper. *) + Definition one_shot_example : val := λ: <>, let: "x" := ref NONE in ( (* tryset *) (λ: "n", diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v index 986b021eeabf807cfd1585e28686fcdd17c14aa2..ad8ea81479c2ff18ddf1133a436351174dd8dac9 100644 --- a/tests/one_shot_once.v +++ b/tests/one_shot_once.v @@ -6,6 +6,9 @@ From iris.proofmode Require Import tactics. From iris.heap_lang.lib Require Import par. Set Default Proof Using "Type". +(** This is the introductory example from Ralf's PhD thesis. +The difference to [one_shot] is that [set] asserts to be called only once. *) + Definition one_shot_example : val := λ: <>, let: "x" := ref NONE in ( (* set *) (λ: "n",