diff options
Diffstat (limited to 'Common')
| -rw-r--r-- | Common/BitVec.lean | 11 | ||||
| -rw-r--r-- | Common/Nat.lean | 3 | ||||
| -rw-r--r-- | Common/Parsing.lean | 6 |
3 files changed, 20 insertions, 0 deletions
diff --git a/Common/BitVec.lean b/Common/BitVec.lean new file mode 100644 index 0000000..ad46efb --- /dev/null +++ b/Common/BitVec.lean @@ -0,0 +1,11 @@ +def BitVec.setBitTrue {n : Nat} (i : Fin n) (a : BitVec n) : BitVec n := + a ||| BitVec.ofNatLt (1 <<< i.val) (by simp[Nat.shiftLeft_eq, i.isLt, Nat.pow_lt_pow_iff_right]) + +def BitVec.setBitFalse {n : Nat} (i : Fin n) (a : BitVec n) : BitVec n := + a &&& BitVec.not (BitVec.ofNatLt (1 <<< i.val) (by simp[Nat.shiftLeft_eq, i.isLt, Nat.pow_lt_pow_iff_right])) + +def BitVec.setBit {n : Nat} (i : Fin n) (v : Bool) (a : BitVec n) : BitVec n := + if v then + a.setBitTrue i + else + a.setBitFalse i diff --git a/Common/Nat.lean b/Common/Nat.lean index 9d0ee29..bc66a09 100644 --- a/Common/Nat.lean +++ b/Common/Nat.lean @@ -23,3 +23,6 @@ theorem lt_of_pred_lt {a b : Nat} (h₁ : a < b.pred) : (a < b) := theorem lt_imp_pred_lt {a b : Nat} (h₁ : a < b) : (a.pred < b) := Nat.lt_of_le_of_lt (Nat.pred_le a) h₁ + +theorem le_of_add_le {a b c d : Nat} (h₁ : a ≤ b + c) (h₂ : c ≤ d) : a ≤ b + d := + Nat.le_trans h₁ (Nat.add_le_add_left h₂ b) diff --git a/Common/Parsing.lean b/Common/Parsing.lean index c811319..348db25 100644 --- a/Common/Parsing.lean +++ b/Common/Parsing.lean @@ -21,6 +21,12 @@ structure RectangularGrid.Coordinate (grid : RectangularGrid Element) where x : Fin grid.width y : Fin grid.height +instance {grid : RectangularGrid Element} : BEq grid.Coordinate where + beq := λa b ↦ a.x == b.x && a.y == b.y + +instance {grid : RectangularGrid Element} : Hashable grid.Coordinate where + hash := λa ↦ Hashable.hash (a.x, a.y) + instance : ToString (RectangularGrid.Coordinate grid) where toString := λx ↦ s!"x: {x.x}/{grid.width}, y : {x.y}/{grid.height}" |