Commit d2dcdaf6 authored by Michael Sammler's avatar Michael Sammler Committed by Paul
Browse files

don't make offset and width reserved identifiers

parent 8eb639e0
......@@ -12,8 +12,8 @@ Local Open Scope bf_scope.
Definition range : Type := nat * nat.
Definition range_of (a k : Z) : range := (Z.to_nat a, Z.to_nat (k - 1)).
Notation "'offset' r" := (fst r) (at level 40) : bf_scope.
Notation "'width' r" := (S (snd r)) (at level 40) : bf_scope. (* always positive *)
Notation offset r := (fst r).
Notation width r := (S (snd r)).
Definition range_eqb (r1 r2 : range) : bool :=
(offset r1 =? offset r2)%nat && (width r1 =? width r2)%nat.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment