Cairn · module

Cairn.UI.Node

lean/Cairn/UI/Node.lean

What view returns (Node) and what layout produces (Laid).

A Node says what is on screen and how it wants to be sized; layout turns it into a Laid with every rect and clip resolved. A node that performs a move carries a Control naming the claim, which is how presence, pressability and the accessibility mirror find it.

Imports Cairn.Geometry, Cairn.Claim, Cairn.Font, Cairn.Effects, Cairn.Input

Order

Structures 17

structure

Cairn.Color

lean/Cairn/UI/Node.lean:20
Color : Type
Fields
r : UInt8
g : UInt8
b : UInt8
a : UInt8
Instances

BEq Inhabited Repr

structure

Cairn.Border

lean/Cairn/UI/Node.lean:45
Border : Type
Fields
width : Nat
color : Color
Instances

BEq Repr Inhabited

structure

Cairn.Shadow

lean/Cairn/UI/Node.lean:60
Shadow : Type

A soft shadow under a box's shape, as SwiftUI's shadow(color:radius:x:y:): the shape's silhouette in color, blurred by radius points and moved by (x, y). With no offset it is a glow.

Fields
color : Color
radius : Nat
x : Int
y : Int
Instances

Inhabited BEq Repr

structure

Cairn.Paint

lean/Cairn/UI/Node.lean:70
Paint : Type

Pixels the host draws: the shader registered under shader fills the box, fed with these numbers (what they mean is the shader's contract) and with the host's clock, as milliseconds since origin (a time on the runtime's monotonic clock), so it can move between frames.

Fields
shader : String
origin : Nat
scalars : List Int
arrays : List (List Int)
Instances

BEq Repr Inhabited

structure

Cairn.ImageFill

lean/Cairn/UI/Node.lean:87
ImageFill : Type

Host-drawn pixels from a loaded image: the host paints the image it holds for source into the box as fit says. width and height are its size in pixels, as the load answered (Reply.image); Lean places it from them (Frame.imageDest), so the host only scales.

Fields
source : String
width : Nat
height : Nat
fit : Fit
Instances

Inhabited BEq Repr

structure

Cairn.VList.Row

lean/Cairn/UI/Node.lean:102
Row : Type

A row whose height is known: it was laid at that height.

Fields
index : Nat

Its place in the list's keys.

key : Nat
height : Nat

Its height as laid, at least one point.

Instances

Repr Inhabited BEq

structure

Cairn.VList.Anchor

lean/Cairn/UI/Node.lean:114
Anchor : Type

The row the reader is at: the first row showing at the offset offset, whose top in the list's content was top in the heights it was recorded with. A row the clamp kept from its place within a batch is held: the place to keep it at is hold points below where it is (VList.anchorAt), until the batch's frame is shown (Known.letGo).

Fields
key : Nat
top : Int
offset : Int
hold : Int
Instances

BEq Inhabited Repr

structure

Cairn.VList.Known

lean/Cairn/UI/Node.lean:124
Known : Type

What the runtime knows of one list (UI.lists), recorded after every layout: the heights of the rows it has laid, sorted by index, at the width they were laid at; the box's length; and the anchor.

Fields
width : Int

The width the rows were laid at: a different width forgets every height.

count : Nat

The number of rows when they were recorded.

rows : Array Row
viewport : Int

The box's length the last time it was laid; 0 before then.

anchor : Option Anchor
est : Nat

The estimate for the rows not yet laid: the mean of the first heights recorded at this width, kept until the width changes, so that recording more heights doesn't move every row below them; 0 before any.

Instances

Inhabited Repr BEq

structure

Cairn.VList.Info

lean/Cairn/UI/Node.lean:145
Info : Type

What a laid virtual list says of itself (Style.rows), for the runtime to record and the fuzzer to check: what the view read, the heights it laid out by, and the window it laid.

Fields
known : Known

What the runtime knew when the view ran (UI.listOf).

model : Array Row

The known heights for these keys (VList.model): known.rows moved to the keys' indices.

keys : Array Nat
estimate : Option Nat

The estimate the view was given, if any, and the one it used.

est : Nat
overscan : Nat
viewport : Int
first : Nat

The rows laid: indices [first, last).

last : Nat
Instances

BEq Repr Inhabited

structure

Cairn.Control

lean/Cairn/UI/Node.lean:171
Control : Type

A node that performs a move.

Fields
role : Role
label : String
value : String
checked : Option Bool
selected : Bool
appear : Bool

Tell the app when this control comes on screen: the runtime delivers Action.appear when it has a visible part at the end of a batch and didn't at the end of the last one (or wasn't in the tree). How an app hears that the end of a list is in view (docs/runtime.md, "Appear").

Instances

Inhabited Repr BEq

structure

Cairn.Shortcut

lean/Cairn/UI/Node.lean:189
Shortcut : Type

A keyboard shortcut shown on a menu item (⌘Q). A status item's and a control's menu honour it only while open; an item in the app's menu bar (Surface.menuBar) has it whenever the app is active (a key equivalent).

Fields
key : Key
mods : Mods
Instances

Repr Inhabited

structure

Cairn.ControlMenu

lean/Cairn/UI/Node.lean:214
ControlMenu : Type

A control's menu (docs/surfaces.md, "Menus on controls"): a native menu the runtime opens over the control, built like a status item's. The secondary click on the control (or on anything inside it that has no menu of its own), the context-menu key (Shift-F10) while it has focus and VoiceOver's Show Menu open it; with button, the control is a menu button (⋯) and a primary click, Space or Return open it too, instead of pressing it. Choosing an item is a press of that item's control (Event.menuSelect with the window's place); opening and closing reach no update. A menu with no items is no menu.

Fields
items : List MenuItem
button : Bool
Instances

BEq Repr Inhabited

structure

Cairn.Style

lean/Cairn/UI/Node.lean:227
Style : Type
Fields
axis : Axis
width : Sizing
height : Sizing
padding : Insets
gap : Nat
align : Align

Cross-axis alignment of children.

justify : Align

Main-axis placement of children when there's space left over.

background : Option Color
border : Option Border
radius : Nat
clip : Bool

Clip children to this box.

corner : Corner
shadow : Option Shadow

Painted under the box's background.

paint : Option Paint

Host-drawn pixels over the background, under the children.

image : Option ImageFill

A loaded image over the background (and the paint), under the children.

scroll : Option Int

A scroll box: some o lays the children out as the box's axis says, then moves them back by o points along that axis (up, or left in a row), and clips them to the box. none is an ordinary box. The children keep their real rects, possibly above or below the box; what shows is rect ∩ clip (docs/layout.md, "Scroll boxes").

scrollRef : Option ControlRef

The scroll box's identity, when the runtime owns its offset (docs/runtime.md, "Scrolling"): the wheel, the trackpad and the page keys move it, and the view reads it back with UI.scrollOf (UI.scrolling sets both fields). Usually a place claim's ref. A box with scroll and no scrollRef scrolls only as far as the view says.

rows : Option VList.Info

A virtual list's box (Cairn.VList): which rows it laid and the heights it laid them by. The runtime records the rows' real heights from it after every layout. Set by VList.node only.

menu : Option ControlMenu

The menu of this box's control (ControlMenu); ignored on a box without a control.

Instances

Repr BEq Inhabited

structure

Cairn.TextStyle

lean/Cairn/UI/Node.lean:269
TextStyle : Type
Fields
font : Font
color : Color
Instances

Inhabited BEq Repr

structure

Cairn.FieldView

lean/Cairn/UI/Node.lean:276
FieldView : Type

What a text field shows. Indices are Unicode scalar positions into text. The editing model that produces this lives in Cairn.Text.

Fields
text : String
caret : Nat
anchor : Nat

Selection is [min anchor caret, max anchor caret).

marked : Option (Nat × Nat)

IME composition in progress, as a range of text.

placeholder : String
focused : Bool
secure : Bool

A secure field (a password): text is one bullet per scalar of what was typed (Cairn.Text.SecureField.view), so it is drawn, measured and dumped as bullets; the frame marks it so the accessibility mirror shows an AXSecureTextField with no value and the host turns on secure event input while it has focus (docs/text.md, "Secure fields").

Instances

Inhabited Repr BEq

structure

Cairn.Wrap

lean/Cairn/UI/Node.lean:300
Wrap : Type

How a wrapped text (Node.para) is sized and broken into lines. The rules are in docs/layout.md ("Wrapped text") and Cairn.Text.Wrap.

Fields
width : Sizing

fixed n wraps at n; hug and fill wrap at the width the parent offers. fill then takes the parent's whole cross or leftover length; hug the widest line.

height : Sizing

hug is the lines' height (lines × line height). A shorter fixed height clips.

maxLines : Option Nat

Keep at most this many lines.

keep : Keep
align : Align

Where each line sits in the width: start (and stretch) left, center, finish right.

lineSpacing : Nat

Points between lines (SwiftUI's lineSpacing).

Instances

Repr Inhabited BEq

structure

Cairn.Image

lean/Cairn/UI/Node.lean:369
Image : Type

An image on screen (Node.image): where its pixels come from (a file path, ~/ for the home folder, or an http/https URL; the host loads it for Request.loadImage), the box it takes in logical points, and what is known of it so far. The box is the same in every state, so nothing moves when the pixels arrive or fail (Layout.measure_image).

Fields
source : String
width : Nat
height : Nat
state : ImageState
fit : Fit
placeholder : Color

The box while loading.

backdrop : Option Color

Under a loaded image: what shows through its transparency and contain's bands.

failedFill : Color

The box, and the colour of its border and words, when the load failed.

failedInk : Color
Instances

Repr Inhabited

Inductive types 11

inductive

Cairn.Axis

lean/Cairn/UI/Node.lean:29
Axis : Type

row and column lay children out along an axis; stack puts them on top of each other, later children on top.

Constructors
row : Axis
column : Axis
stack : Axis
Instances

Inhabited Repr BEq

inductive

Cairn.Align

lean/Cairn/UI/Node.lean:33
Align : Type
Constructors
start : Align
center : Align
finish : Align
stretch : Align
Instances

Repr Inhabited BEq

inductive

Cairn.Sizing

lean/Cairn/UI/Node.lean:40
Sizing : Type

fill shares the parent's leftover main-axis space equally among fill children, and takes the parent's full cross-axis size.

Constructors
fixed (n : Nat) : Sizing
hug : Sizing
fill : Sizing
Instances

Repr Inhabited BEq

inductive

Cairn.Corner

lean/Cairn/UI/Node.lean:53
Corner : Type

How a rounded box's corners turn: a circular arc, or Apple's continuous curve (SwiftUI's RoundedRectangle(style: .continuous)), which starts further along the edge and has no jump in curvature.

Constructors
circular : Corner
continuous : Corner
Instances

Repr BEq Inhabited

inductive

Cairn.Fit

lean/Cairn/UI/Node.lean:80
Fit : Type

How an image's pixels fill its box: stretched to it (fill), scaled to fit inside it with the aspect ratio kept (contain, centred, leaving bands), or scaled to cover it with the aspect ratio kept (cover, centred, cut by the box).

Constructors
fill : Fit
contain : Fit
cover : Fit
Instances

Inhabited BEq Repr

inductive

Cairn.Role

lean/Cairn/UI/Node.lean:164
Role : Type
Constructors
group : Role
button : Role
checkbox : Role
text : Role
textField : Role
list : Role
listItem : Role
heading : Role
tab : Role
scrollArea : Role

A scroll box (Style.scroll): the frame gives one a node of its own.

Instances

Repr BEq Inhabited

inductive

Cairn.MenuItem

lean/Cairn/UI/Node.lean:196
MenuItem : Type

One entry of a native menu: a status item's, a control's (ControlMenu) or the app's own in the menu bar (docs/surfaces.md). The host builds a real NSMenu from it.

Constructors
item (control : Control) (enabled : Bool := true)
  (shortcut : Option Shortcut := none) : MenuItem

An item that performs a move. control.checked = some b makes it a checkbox item; enabled = false greys it out (it stays in the menu, with its control).

info (label : String) : MenuItem

A line of text that does nothing: a status line, "None yet". Shown disabled.

submenu (label : String) (place : Option ClaimId) (items : List MenuItem) :
  MenuItem

A submenu. place is the place claim it is, if it has one.

separator : MenuItem
Instances

Inhabited Repr BEq

inductive

Cairn.Keep

lean/Cairn/UI/Node.lean:294
Keep : Type

Which lines a wrapped text keeps when it has more than maxLines: the first ones, or the last ones (a growing transcript that shows its end).

Constructors
head : Keep
tail : Keep
Instances

BEq Repr Inhabited

inductive

Cairn.Node

lean/Cairn/UI/Node.lean:316
Node : Type
Constructors
box (style : Style) (control : Option Control) (children : List Node) : Node
text (style : TextStyle) (content : String) : Node
para (style : TextStyle) (wrap : Wrap) (content : String) : Node

Text wrapped at word boundaries to the available width (Cairn.Text.Wrap). Layout turns it into a clipping column of one text per line, so it has no Laid form of its own.

field (style : Style) (text : TextStyle) (control : Control) (view : FieldView) :
  Node
Instances

Inhabited Repr

inductive

Cairn.Laid

lean/Cairn/UI/Node.lean:328
Laid : Type

A laid-out node. clip is the region this node may paint in (the intersection of every clipping ancestor), so the visible part of a node is rect.inter clip.

Constructors
box (rect clip : Rect) (style : Style) (control : Option Control)
  (children : List Laid) : Laid
text (rect clip : Rect) (baseline : Int) (style : TextStyle) (content : String) :
  Laid
field (rect clip : Rect) (style : Style) (text : TextStyle) (control : Control)
  (view : FieldView) (textOrigin : Point) (caret : Rect) (selection : List Rect) : Laid
Instances

Inhabited Repr

inductive

Cairn.ImageState

lean/Cairn/UI/Node.lean:359
ImageState : Type

What an app knows of an image so far: not loaded yet, loaded (its size in pixels, from Reply.image), or failed (from Reply.failed).

Constructors
loading : ImageState
ready (width height : Nat) : ImageState
failed (fault : Fault) (message : String) : ImageState
Instances

Repr Inhabited

Definitions 11

def

Cairn.VList.Known.letGo

lean/Cairn/UI/Node.lean:141
letGo (k : Known) : Known

What is known once a frame is shown: a held anchor is let go, so the row is kept where it now shows.

def

Cairn.ControlMenu.mark

lean/Cairn/UI/Node.lean:221
mark : Option ControlMenu → Option Bool

What the accessibility mirror says of a menu: some true a menu button, some false a context menu, none no menu (or one with no items).

def

Cairn.Laid.rect

lean/Cairn/UI/Node.lean:337
rect : Laid → Rect
def

Cairn.Laid.clip

lean/Cairn/UI/Node.lean:340
clip : Laid → Rect
def

Cairn.Laid.visible

lean/Cairn/UI/Node.lean:343
visible (l : Laid) : Rect
def

Cairn.Laid.control?

lean/Cairn/UI/Node.lean:345
control? : Laid → Option Control
def

Cairn.Laid.menu?

lean/Cairn/UI/Node.lean:351
menu? : Laid → Option ControlMenu

The menu of the node's control (Style.menu), if it has items.

def

Cairn.Image.faultText

lean/Cairn/UI/Node.lean:385
faultText : Fault → String

The words a failed image shows.

def

Cairn.Image.style

lean/Cairn/UI/Node.lean:391
style (i : Image) : Style

The image's box: fixed at its size in every state, clipping; the placeholder colour while loading, the pixels once loaded, a bordered box with the fault's words when failed.

def

Cairn.Image.children

lean/Cairn/UI/Node.lean:406
children (i : Image) : List Node

What a failed image says, centred in its box (clipped to it); nothing otherwise.

def

Cairn.Node.image

lean/Cairn/UI/Node.lean:416
image (i : Image) : Node

An image node. A box of the image's size whatever its state, so layout knows its size before the pixels exist; it has no control (an image is not a move) and paints, from back to front, its state's background, the host's pixels once loaded (Style.image), and a failure's words.

Instances 96

instance

Cairn.instBEqColor

lean/Cairn/UI/Node.lean:25
instBEqColor : BEq Color
instance

Cairn.instInhabitedColor

lean/Cairn/UI/Node.lean:25
instInhabitedColor : Inhabited Color
instance

Cairn.instDecidableEqColor

lean/Cairn/UI/Node.lean:25
instDecidableEqColor : DecidableEq Color
instance

Cairn.instReprColor

lean/Cairn/UI/Node.lean:25
instReprColor : Repr Color
instance

Cairn.instInhabitedAxis

lean/Cairn/UI/Node.lean:31
instInhabitedAxis : Inhabited Axis
instance

Cairn.instReprAxis

lean/Cairn/UI/Node.lean:31
instReprAxis : Repr Axis
instance

Cairn.instDecidableEqAxis

lean/Cairn/UI/Node.lean:31
instDecidableEqAxis : DecidableEq Axis
instance

Cairn.instBEqAxis

lean/Cairn/UI/Node.lean:31
instBEqAxis : BEq Axis
instance

Cairn.instReprAlign

lean/Cairn/UI/Node.lean:35
instReprAlign : Repr Align
instance

Cairn.instDecidableEqAlign

lean/Cairn/UI/Node.lean:35
instDecidableEqAlign : DecidableEq Align
instance

Cairn.instInhabitedAlign

lean/Cairn/UI/Node.lean:35
instInhabitedAlign : Inhabited Align
instance

Cairn.instBEqAlign

lean/Cairn/UI/Node.lean:35
instBEqAlign : BEq Align
instance

Cairn.instDecidableEqSizing

lean/Cairn/UI/Node.lean:42
instDecidableEqSizing : DecidableEq Sizing
instance

Cairn.instReprSizing

lean/Cairn/UI/Node.lean:42
instReprSizing : Repr Sizing
instance

Cairn.instInhabitedSizing

lean/Cairn/UI/Node.lean:42
instInhabitedSizing : Inhabited Sizing
instance

Cairn.instBEqSizing

lean/Cairn/UI/Node.lean:42
instBEqSizing : BEq Sizing
instance

Cairn.instBEqBorder

lean/Cairn/UI/Node.lean:48
instBEqBorder : BEq Border
instance

Cairn.instReprBorder

lean/Cairn/UI/Node.lean:48
instReprBorder : Repr Border
instance

Cairn.instDecidableEqBorder

lean/Cairn/UI/Node.lean:48
instDecidableEqBorder : DecidableEq Border
instance

Cairn.instInhabitedBorder

lean/Cairn/UI/Node.lean:48
instInhabitedBorder : Inhabited Border
instance

Cairn.instReprCorner

lean/Cairn/UI/Node.lean:55
instReprCorner : Repr Corner
instance

Cairn.instBEqCorner

lean/Cairn/UI/Node.lean:55
instBEqCorner : BEq Corner
instance

Cairn.instInhabitedCorner

lean/Cairn/UI/Node.lean:55
instInhabitedCorner : Inhabited Corner
instance

Cairn.instDecidableEqCorner

lean/Cairn/UI/Node.lean:55
instDecidableEqCorner : DecidableEq Corner
instance

Cairn.instInhabitedShadow

lean/Cairn/UI/Node.lean:65
instInhabitedShadow : Inhabited Shadow
instance

Cairn.instBEqShadow

lean/Cairn/UI/Node.lean:65
instBEqShadow : BEq Shadow
instance

Cairn.instDecidableEqShadow

lean/Cairn/UI/Node.lean:65
instDecidableEqShadow : DecidableEq Shadow
instance

Cairn.instReprShadow

lean/Cairn/UI/Node.lean:65
instReprShadow : Repr Shadow
instance

Cairn.instBEqPaint

lean/Cairn/UI/Node.lean:75
instBEqPaint : BEq Paint
instance

Cairn.instDecidableEqPaint

lean/Cairn/UI/Node.lean:75
instDecidableEqPaint : DecidableEq Paint
instance

Cairn.instReprPaint

lean/Cairn/UI/Node.lean:75
instReprPaint : Repr Paint
instance

Cairn.instInhabitedPaint

lean/Cairn/UI/Node.lean:75
instInhabitedPaint : Inhabited Paint
instance

Cairn.instInhabitedFit

lean/Cairn/UI/Node.lean:82
instInhabitedFit : Inhabited Fit
instance

Cairn.instBEqFit

lean/Cairn/UI/Node.lean:82
instBEqFit : BEq Fit
instance

Cairn.instDecidableEqFit

lean/Cairn/UI/Node.lean:82
instDecidableEqFit : DecidableEq Fit
instance

Cairn.instReprFit

lean/Cairn/UI/Node.lean:82
instReprFit : Repr Fit
instance

Cairn.instInhabitedImageFill

lean/Cairn/UI/Node.lean:92
instInhabitedImageFill : Inhabited ImageFill
instance

Cairn.instBEqImageFill

lean/Cairn/UI/Node.lean:92
instBEqImageFill : BEq ImageFill
instance

Cairn.instReprImageFill

lean/Cairn/UI/Node.lean:92
instReprImageFill : Repr ImageFill
instance

Cairn.instDecidableEqImageFill

lean/Cairn/UI/Node.lean:92
instDecidableEqImageFill : DecidableEq ImageFill
instance

Cairn.VList.instDecidableEqRow

lean/Cairn/UI/Node.lean:108
instDecidableEqRow : DecidableEq Row
instance

Cairn.VList.instReprRow

lean/Cairn/UI/Node.lean:108
instReprRow : Repr Row
instance

Cairn.VList.instInhabitedRow

lean/Cairn/UI/Node.lean:108
instInhabitedRow : Inhabited Row
instance

Cairn.VList.instBEqRow

lean/Cairn/UI/Node.lean:108
instBEqRow : BEq Row
instance

Cairn.VList.instDecidableEqAnchor

lean/Cairn/UI/Node.lean:119
instDecidableEqAnchor : DecidableEq Anchor
instance

Cairn.VList.instBEqAnchor

lean/Cairn/UI/Node.lean:119
instBEqAnchor : BEq Anchor
instance

Cairn.VList.instInhabitedAnchor

lean/Cairn/UI/Node.lean:119
instInhabitedAnchor : Inhabited Anchor
instance

Cairn.VList.instReprAnchor

lean/Cairn/UI/Node.lean:119
instReprAnchor : Repr Anchor
instance

Cairn.VList.instInhabitedKnown

lean/Cairn/UI/Node.lean:137
instInhabitedKnown : Inhabited Known
instance

Cairn.VList.instReprKnown

lean/Cairn/UI/Node.lean:137
instReprKnown : Repr Known
instance

Cairn.VList.instBEqKnown

lean/Cairn/UI/Node.lean:137
instBEqKnown : BEq Known
instance

Cairn.VList.instDecidableEqKnown

lean/Cairn/UI/Node.lean:137
instDecidableEqKnown : DecidableEq Known
instance

Cairn.VList.instBEqInfo

lean/Cairn/UI/Node.lean:159
instBEqInfo : BEq Info
instance

Cairn.VList.instReprInfo

lean/Cairn/UI/Node.lean:159
instReprInfo : Repr Info
instance

Cairn.VList.instInhabitedInfo

lean/Cairn/UI/Node.lean:159
instInhabitedInfo : Inhabited Info
instance

Cairn.instReprRole

lean/Cairn/UI/Node.lean:168
instReprRole : Repr Role
instance

Cairn.instDecidableEqRole

lean/Cairn/UI/Node.lean:168
instDecidableEqRole : DecidableEq Role
instance

Cairn.instBEqRole

lean/Cairn/UI/Node.lean:168
instBEqRole : BEq Role
instance

Cairn.instInhabitedRole

lean/Cairn/UI/Node.lean:168
instInhabitedRole : Inhabited Role
instance

Cairn.instInhabitedControl

lean/Cairn/UI/Node.lean:182
instInhabitedControl : Inhabited Control
instance

Cairn.instReprControl

lean/Cairn/UI/Node.lean:182
instReprControl : Repr Control
instance

Cairn.instBEqControl

lean/Cairn/UI/Node.lean:182
instBEqControl : BEq Control
instance

Cairn.instDecidableEqShortcut

lean/Cairn/UI/Node.lean:192
instDecidableEqShortcut : DecidableEq Shortcut
instance

Cairn.instReprShortcut

lean/Cairn/UI/Node.lean:192
instReprShortcut : Repr Shortcut
instance

Cairn.instInhabitedShortcut

lean/Cairn/UI/Node.lean:192
instInhabitedShortcut : Inhabited Shortcut
instance

Cairn.instInhabitedMenuItem

lean/Cairn/UI/Node.lean:205
instInhabitedMenuItem : Inhabited MenuItem
instance

Cairn.instReprMenuItem

lean/Cairn/UI/Node.lean:205
instReprMenuItem : Repr MenuItem
instance

Cairn.instBEqMenuItem

lean/Cairn/UI/Node.lean:205
instBEqMenuItem : BEq MenuItem
instance

Cairn.instBEqControlMenu

lean/Cairn/UI/Node.lean:217
instBEqControlMenu : BEq ControlMenu
instance

Cairn.instReprControlMenu

lean/Cairn/UI/Node.lean:217
instReprControlMenu : Repr ControlMenu
instance

Cairn.instInhabitedControlMenu

lean/Cairn/UI/Node.lean:217
instInhabitedControlMenu : Inhabited ControlMenu
instance

Cairn.instReprStyle

lean/Cairn/UI/Node.lean:265
instReprStyle : Repr Style
instance

Cairn.instBEqStyle

lean/Cairn/UI/Node.lean:265
instBEqStyle : BEq Style
instance

Cairn.instInhabitedStyle

lean/Cairn/UI/Node.lean:265
instInhabitedStyle : Inhabited Style
instance

Cairn.instInhabitedTextStyle

lean/Cairn/UI/Node.lean:272
instInhabitedTextStyle : Inhabited TextStyle
instance

Cairn.instBEqTextStyle

lean/Cairn/UI/Node.lean:272
instBEqTextStyle : BEq TextStyle
instance

Cairn.instReprTextStyle

lean/Cairn/UI/Node.lean:272
instReprTextStyle : Repr TextStyle
instance

Cairn.instInhabitedFieldView

lean/Cairn/UI/Node.lean:290
instInhabitedFieldView : Inhabited FieldView
instance

Cairn.instReprFieldView

lean/Cairn/UI/Node.lean:290
instReprFieldView : Repr FieldView
instance

Cairn.instBEqFieldView

lean/Cairn/UI/Node.lean:290
instBEqFieldView : BEq FieldView
instance

Cairn.instDecidableEqKeep

lean/Cairn/UI/Node.lean:296
instDecidableEqKeep : DecidableEq Keep
instance

Cairn.instBEqKeep

lean/Cairn/UI/Node.lean:296
instBEqKeep : BEq Keep
instance

Cairn.instReprKeep

lean/Cairn/UI/Node.lean:296
instReprKeep : Repr Keep
instance

Cairn.instInhabitedKeep

lean/Cairn/UI/Node.lean:296
instInhabitedKeep : Inhabited Keep
instance

Cairn.instReprWrap

lean/Cairn/UI/Node.lean:313
instReprWrap : Repr Wrap
instance

Cairn.instInhabitedWrap

lean/Cairn/UI/Node.lean:313
instInhabitedWrap : Inhabited Wrap
instance

Cairn.instBEqWrap

lean/Cairn/UI/Node.lean:313
instBEqWrap : BEq Wrap
instance

Cairn.instInhabitedNode

lean/Cairn/UI/Node.lean:323
instInhabitedNode : Inhabited Node
instance

Cairn.instReprNode

lean/Cairn/UI/Node.lean:323
instReprNode : Repr Node
instance

Cairn.instInhabitedLaid

lean/Cairn/UI/Node.lean:333
instInhabitedLaid : Inhabited Laid
instance

Cairn.instReprLaid

lean/Cairn/UI/Node.lean:333
instReprLaid : Repr Laid
instance

Cairn.instReprImageState

lean/Cairn/UI/Node.lean:363
instReprImageState : Repr ImageState
instance

Cairn.instInhabitedImageState

lean/Cairn/UI/Node.lean:363
instInhabitedImageState : Inhabited ImageState
instance

Cairn.instDecidableEqImageState

lean/Cairn/UI/Node.lean:363
instDecidableEqImageState : DecidableEq ImageState
instance

Cairn.instReprImage

lean/Cairn/UI/Node.lean:382
instReprImage : Repr Image
instance

Cairn.instInhabitedImage

lean/Cairn/UI/Node.lean:382
instInhabitedImage : Inhabited Image