diff options
Diffstat (limited to 'src/Assembly/QhasmCommon.v')
| -rw-r--r-- | src/Assembly/QhasmCommon.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Assembly/QhasmCommon.v b/src/Assembly/QhasmCommon.v index 654f109f3..ccec401d2 100644 --- a/src/Assembly/QhasmCommon.v +++ b/src/Assembly/QhasmCommon.v @@ -4,7 +4,7 @@ Require Export Bedrock.Word. (* Utilities *) Definition Label := nat. -Definition Index (limit: nat) := {x: nat | (x < limit)%nat}. +Definition Index (limit: nat) := {x: nat | (x <= (pred limit))%nat}. Coercion indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i. Inductive Either A B := |