Cairn · module
Cairn.Geometry
lean/Cairn/Geometry.lean
Geometry in integer logical points, origin top-left, y down. No floats anywhere a theorem looks. The host multiplies by the backing scale when it paints.
Order
Structures 4
Point : Type
Fields
x : Inty : IntSize : Type
Fields
w : Inth : IntRect : Type
Fields
x : Inty : Intw : Inth : IntInsets : Type
Fields
top : Intright : Intbottom : Intleft : IntDefinitions 7
contains (r : Rect) (p : Point) : Bool
center (r : Rect) : Point
The point a click on this rect is aimed at. Inside the rect whenever w > 0 ∧ h > 0.
inside (r o : Rect) : Prop
r lies entirely within o.
Instances
disjoint (a b : Rect) : Prop
nonempty (r : Rect) : Prop
Instances
inset (r : Rect) (i : Insets) : Rect
inter (a b : Rect) : Rect
Intersection, used for clipping. Width and height floor at zero. When the rects don't
overlap, the empty result is placed inside a (its origin is clamped to a's far edge), so
a.inter b is inside a whenever a has non-negative size.
Instances 18
instDecidableEqPoint : DecidableEq Point
instBEqPoint : BEq Point
instReprPoint : Repr Point
instInhabitedPoint : Inhabited Point
instBEqSize : BEq Size
instInhabitedSize : Inhabited Size
instReprSize : Repr Size
instDecidableEqSize : DecidableEq Size
instReprRect : Repr Rect
instBEqRect : BEq Rect
instDecidableEqRect : DecidableEq Rect
instInhabitedRect : Inhabited Rect
instBEqInsets : BEq Insets
instReprInsets : Repr Insets
instDecidableEqInsets : DecidableEq Insets
instInhabitedInsets : Inhabited Insets
instDecidableInside (r o : Rect) : Decidable (r.inside o)
instDecidableNonempty (r : Rect) : Decidable r.nonempty