Documentation

Projects.AP.Defense.Edge.Symmetry.Rotation

def AP.Edge.rotRight (e : Edge) :

Equations

e.rotRight = { dir := e.dir.rotRight, offset := if e.hor then -e.offset else e.offset }

Instances For

def AP.Edge.rotLeft (e : Edge) :

Equations

e.rotLeft = { dir := e.dir.rotLeft, offset := if e.hor then e.offset else -e.offset }

Instances For

def AP.Edge.rot180 (e : Edge) :

Equations

e.rot180 = { dir := e.dir⁻¹, offset := -e.offset }

Instances For

@[simp]

theorem AP.Edge.points_rotRight {e : Edge} :

e.rotRight.points = ⇑rotRight.ft '' e.points

@[simp]

theorem AP.Edge.points_rotLeft {e : Edge} :

e.rotLeft.points = ⇑rotLeft.ft '' e.points

@[simp]

theorem AP.Edge.dist_rotRight {e : Edge} {p : PointZ} :

e.rotRight.dist p = e.dist (rotRight.ft' p)

@[simp]

theorem AP.Edge.getBorderPoint_rotRight {e : Edge} {p : PointZ} {d : ℤ} :

e.rotRight.getBorderPoint p d = rotRight.ft (e.getBorderPoint (rotRight.ft' p) d)

@[simp]

theorem AP.Edge.getBorderPoint₀_rotRight {e : Edge} {p : PointZ} :

e.rotRight.getBorderPoint₀ p = rotRight.ft (e.getBorderPoint₀ (rotRight.ft' p))

@[simp]

theorem AP.Edge.getBorderPoints_rotRight {e : Edge} {p : PointZ} {d : ℕ} :

e.rotRight.getBorderPoints p d = List.map (⇑rotRight.ft) (e.getBorderPoints (rotRight.ft' p) d)

@[simp]

theorem AP.Edge.dir_rotRight {e : Edge} :

e.rotRight.dir = e.dir.rotRight

@[simp]

theorem AP.Edge.offset_rotRight_eq_of_hor {e : Edge} [H : Fact e.hor] :

e.rotRight.offset = -e.offset

@[simp]

theorem AP.Edge.offset_rotRight_eq_of_vert {e : Edge} [H : Fact e.vert] :

e.rotRight.offset = e.offset

@[simp]

theorem AP.Edge.rotRight_rotLeft {e : Edge} :

e.rotLeft.rotRight = e

@[simp]

theorem AP.Edge.rotLeft_rotRight {e : Edge} :

e.rotRight.rotLeft = e

@[simp]

theorem AP.Edge.dir_rotLeft {e : Edge} :

e.rotLeft.dir = e.dir.rotLeft

@[simp]

theorem AP.Edge.ptsArr_rotRight {e : Edge} {s : State} :

e.rotRight.ptsArr s = e.ptsArr (rotRight.fs' s)

@[simp]

theorem AP.Edge.defense_rotRight {e : Edge} :

e.rotRight.defense = e.defense.sym rotRight

@[simp]

theorem AP.Edge.rotRight_rotRight {e : Edge} :

e.rotRight.rotRight = e.rot180

@[simp]

theorem AP.Edge.rotLeft_rotLeft {e : Edge} :

e.rotLeft.rotLeft = e.rot180

@[simp]

theorem AP.Edge.rot180_rotRight {e : Edge} :

e.rotRight.rot180 = e.rotLeft

@[simp]

theorem AP.Edge.defense_rotLeft {e : Edge} :

e.rotLeft.defense = e.defense.sym rotLeft

@[simp]

theorem AP.Edge.defense_rot180 {e : Edge} :

e.rot180.defense = e.defense.sym rot180