Compare revisions

086cc92c · 086cc92c · 086cc92c · 086cc92c · 086cc92c · 086cc92c
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
--- a/heap_lang/lib/assert.v
+++ b/heap_lang/lib/assert.v
--- a/heap_lang/lib/barrier/barrier.v
+++ b/heap_lang/lib/barrier/barrier.v
-From iris.heap_lang Require Export notation.
-
-Definition newbarrier : val := λ: <>, ref #0.
-Definition signal : val := λ: "x", '"x" <- #1.
-Definition wait : val :=
-  rec: "wait" "x" := if: !'"x" = #1 then #() else '"wait" '"x".
-Global Opaque newbarrier signal wait.
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
--- a/heap_lang/lib/barrier/protocol.v
+++ b/heap_lang/lib/barrier/protocol.v
--- a/heap_lang/lib/barrier/specification.v
+++ b/heap_lang/lib/barrier/specification.v
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
--- a/heap_lang/substitution.v
+++ b/heap_lang/substitution.v
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
--- a/iris-bot
+++ b/iris-bot
--- a/iris/algebra/agree.v
+++ b/iris/algebra/agree.v
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
No results found