pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2025-01-08 09:04:14 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Harmonize inductive-definition convention

Browse source
This commit is contained in:
Adam Chlipala 2016-02-16 11:41:30 -05:00
parent 0123f45d21
commit 33d01606bf
2 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
TransitionSystems.v
View file

@ -301,12 +301,12 @@ Qed.
* kinds of *local*state* in a thread: * kinds of *local*state* in a thread:
* - program counter * - program counter
* - values of local variables that may be ready eventually *) * - values of local variables that may be ready eventually *)
Inductive increment_program : Set := Inductive increment_program :=
| Lock : increment_program | Lock
| Read : increment_program | Read
| Write : nat -> increment_program | Write (local : nat)
| Unlock : increment_program | Unlock
| Done : increment_program. | Done.
(* Next, a type for state shared between threads. *) (* Next, a type for state shared between threads. *)
Record inc_state := { Record inc_state := {

12
TransitionSystems_template.v
View file

@ -203,12 +203,12 @@ Qed.
* kinds of *local*state* in a thread: * kinds of *local*state* in a thread:
* - program counter * - program counter
* - values of local variables that may be ready eventually *) * - values of local variables that may be ready eventually *)
Inductive increment_program : Set := Inductive increment_program :=
| Lock : increment_program | Lock
| Read : increment_program | Read
| Write : nat -> increment_program | Write (local : nat)
| Unlock : increment_program | Unlock
| Done : increment_program. | Done.
(* Next, a type for state shared between threads. *) (* Next, a type for state shared between threads. *)
Record inc_state := { Record inc_state := {