pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge pull request #51 from mdempsky/csl-example-typo

Browse source 
Fix typo in ConcurrentSeparationLogic.v example
This commit is contained in:
Adam Chlipala 2021-01-03 14:39:16 -05:00 committed by GitHub
commit 845c9189c1
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
ConcurrentSeparationLogic.v
View file

@ -699,7 +699,7 @@ Qed.
(* Here's a variant on the last example. Now we have three stages. (* Here's a variant on the last example. Now we have three stages.
* Stage 1: push consecutive even numbers to stack 1. * Stage 1: push consecutive even numbers to stack 1.
* Stage 2: pop from stack 1 and push to stack 1, reusing the memory for the * Stage 2: pop from stack 1 and push to stack 2, reusing the memory for the
* list node. * list node.
* Stage 3: pop from stack 2 and fail if odd. *) * Stage 3: pop from stack 2 and fail if odd. *)