structure Lapis.VFS.FingerTree.Measure : Type

Measure for piece table: tracks byte count, UTF-16 units, and line count

• bytes : Nat
• utf16Units : Nat
• lines : Nat

def Lapis.VFS.FingerTree.instReprMeasure.repr : Measure → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.VFS.FingerTree.instReprMeasure : Repr Measure

Equations

• Lapis.VFS.FingerTree.instReprMeasure = { reprPrec := Lapis.VFS.FingerTree.instReprMeasure.repr }

def Lapis.VFS.FingerTree.instInhabitedMeasure.default : Measure

Equations

• Lapis.VFS.FingerTree.instInhabitedMeasure.default = { bytes := default, utf16Units := default, lines := default }

instance Lapis.VFS.FingerTree.instInhabitedMeasure : Inhabited Measure

Equations

• Lapis.VFS.FingerTree.instInhabitedMeasure = { default := Lapis.VFS.FingerTree.instInhabitedMeasure.default }

def Lapis.VFS.FingerTree.instBEqMeasure.beq : Measure → Measure → Bool

Equations

• Lapis.VFS.FingerTree.instBEqMeasure.beq { bytes := a, utf16Units := a_1, lines := a_2 } { bytes := b, utf16Units := b_1, lines := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lapis.VFS.FingerTree.instBEqMeasure.beq x✝¹ x✝ = false

instance Lapis.VFS.FingerTree.instBEqMeasure : BEq Measure

Equations

• Lapis.VFS.FingerTree.instBEqMeasure = { beq := Lapis.VFS.FingerTree.instBEqMeasure.beq }

instance Lapis.VFS.FingerTree.instAddMeasure : Add Measure

Equations

• One or more equations did not get rendered due to their size.

def Lapis.VFS.FingerTree.Measure.empty : Measure

Equations

• Lapis.VFS.FingerTree.Measure.empty = { bytes := 0, utf16Units := 0, lines := 0 }

class Lapis.VFS.FingerTree.Measurable (α : Type) : Type

Typeclass for elements that can be measured

• measure : α → Measure

instance Lapis.VFS.FingerTree.instReprDigit {α✝ : Type} [Repr α✝] : Repr (Lapis.VFS.FingerTree.Digit✝ α✝)

Equations

• Lapis.VFS.FingerTree.instReprDigit = { reprPrec := Lapis.VFS.FingerTree.instReprDigit.repr }

def Lapis.VFS.FingerTree.instReprDigit.repr {α✝ : Type} [Repr α✝] : Lapis.VFS.FingerTree.Digit✝ α✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.VFS.FingerTree.instInhabitedDigit {a✝ : Type} [Inhabited a✝] : Inhabited (Lapis.VFS.FingerTree.Digit✝ a✝)

Equations

• Lapis.VFS.FingerTree.instInhabitedDigit = { default := Lapis.VFS.FingerTree.instInhabitedDigit.default }

def Lapis.VFS.FingerTree.instInhabitedDigit.default {a✝ : Type} [Inhabited a✝] : Lapis.VFS.FingerTree.Digit✝ a✝

Equations

• Lapis.VFS.FingerTree.instInhabitedDigit.default = Lapis.VFS.FingerTree.Digit.one✝ default

def Lapis.VFS.FingerTree.Digit.toList {α : Type} : Lapis.VFS.FingerTree.Digit✝ α → List α

Equations

• Lapis.VFS.FingerTree.Digit.toList (Lapis.VFS.FingerTree.Digit.one✝ a) = [a]
• Lapis.VFS.FingerTree.Digit.toList (Lapis.VFS.FingerTree.Digit.two✝ a a_1) = [a, a_1]
• Lapis.VFS.FingerTree.Digit.toList (Lapis.VFS.FingerTree.Digit.three✝ a a_1 a_2) = [a, a_1, a_2]
• Lapis.VFS.FingerTree.Digit.toList (Lapis.VFS.FingerTree.Digit.four✝ a a_1 a_2 a_3) = [a, a_1, a_2, a_3]

def Lapis.VFS.FingerTree.Digit.toArray {α : Type} : Lapis.VFS.FingerTree.Digit✝ α → Array α

Equations

• Lapis.VFS.FingerTree.Digit.toArray (Lapis.VFS.FingerTree.Digit.one✝ a) = #[a]
• Lapis.VFS.FingerTree.Digit.toArray (Lapis.VFS.FingerTree.Digit.two✝ a a_1) = #[a, a_1]
• Lapis.VFS.FingerTree.Digit.toArray (Lapis.VFS.FingerTree.Digit.three✝ a a_1 a_2) = #[a, a_1, a_2]
• Lapis.VFS.FingerTree.Digit.toArray (Lapis.VFS.FingerTree.Digit.four✝ a a_1 a_2 a_3) = #[a, a_1, a_2, a_3]

def Lapis.VFS.FingerTree.Digit.head {α : Type} : Lapis.VFS.FingerTree.Digit✝ α → α

Equations

• Lapis.VFS.FingerTree.Digit.head (Lapis.VFS.FingerTree.Digit.one✝ a) = a
• Lapis.VFS.FingerTree.Digit.head (Lapis.VFS.FingerTree.Digit.two✝ a a_1) = a
• Lapis.VFS.FingerTree.Digit.head (Lapis.VFS.FingerTree.Digit.three✝ a a_1 a_2) = a
• Lapis.VFS.FingerTree.Digit.head (Lapis.VFS.FingerTree.Digit.four✝ a a_1 a_2 a_3) = a

def Lapis.VFS.FingerTree.Digit.last {α : Type} : Lapis.VFS.FingerTree.Digit✝ α → α

Equations

• Lapis.VFS.FingerTree.Digit.last (Lapis.VFS.FingerTree.Digit.one✝ a) = a
• Lapis.VFS.FingerTree.Digit.last (Lapis.VFS.FingerTree.Digit.two✝ a a_1) = a_1
• Lapis.VFS.FingerTree.Digit.last (Lapis.VFS.FingerTree.Digit.three✝ a a_1 a_2) = a_2
• Lapis.VFS.FingerTree.Digit.last (Lapis.VFS.FingerTree.Digit.four✝ a a_1 a_2 a_3) = a_3

def Lapis.VFS.FingerTree.Digit.tail? {α : Type} : Lapis.VFS.FingerTree.Digit✝ α → Option (Lapis.VFS.FingerTree.Digit✝¹ α)

Equations

• Lapis.VFS.FingerTree.Digit.tail? (Lapis.VFS.FingerTree.Digit.one✝ a) = none
• Lapis.VFS.FingerTree.Digit.tail? (Lapis.VFS.FingerTree.Digit.two✝ a a_1) = some (Lapis.VFS.FingerTree.Digit.one✝ a_1)
• Lapis.VFS.FingerTree.Digit.tail? (Lapis.VFS.FingerTree.Digit.three✝ a a_1 a_2) = some (Lapis.VFS.FingerTree.Digit.two✝ a_1 a_2)
• Lapis.VFS.FingerTree.Digit.tail? (Lapis.VFS.FingerTree.Digit.four✝ a a_1 a_2 a_3) = some (Lapis.VFS.FingerTree.Digit.three✝ a_1 a_2 a_3)

def Lapis.VFS.FingerTree.Digit.init? {α : Type} : Lapis.VFS.FingerTree.Digit✝ α → Option (Lapis.VFS.FingerTree.Digit✝¹ α)

Equations

• Lapis.VFS.FingerTree.Digit.init? (Lapis.VFS.FingerTree.Digit.one✝ a) = none
• Lapis.VFS.FingerTree.Digit.init? (Lapis.VFS.FingerTree.Digit.two✝ a a_1) = some (Lapis.VFS.FingerTree.Digit.one✝ a)
• Lapis.VFS.FingerTree.Digit.init? (Lapis.VFS.FingerTree.Digit.three✝ a a_1 a_2) = some (Lapis.VFS.FingerTree.Digit.two✝ a a_1)
• Lapis.VFS.FingerTree.Digit.init? (Lapis.VFS.FingerTree.Digit.four✝ a a_1 a_2 a_3) = some (Lapis.VFS.FingerTree.Digit.three✝ a a_1 a_2)

def Lapis.VFS.FingerTree.Digit.fromList? {α : Type} : List α → Option (Lapis.VFS.FingerTree.Digit✝ α)

Equations

• Lapis.VFS.FingerTree.Digit.fromList? [a] = some (Lapis.VFS.FingerTree.Digit.one✝ a)
• Lapis.VFS.FingerTree.Digit.fromList? [a, b] = some (Lapis.VFS.FingerTree.Digit.two✝ a b)
• Lapis.VFS.FingerTree.Digit.fromList? [a, b, c] = some (Lapis.VFS.FingerTree.Digit.three✝ a b c)
• Lapis.VFS.FingerTree.Digit.fromList? [a, b, c, d] = some (Lapis.VFS.FingerTree.Digit.four✝ a b c d)
• Lapis.VFS.FingerTree.Digit.fromList? x✝ = none

def Lapis.VFS.FingerTree.Digit.measure {α : Type} [Measurable α] : Lapis.VFS.FingerTree.Digit✝ α → Measure

Equations

• One or more equations did not get rendered due to their size.
• Lapis.VFS.FingerTree.Digit.measure (Lapis.VFS.FingerTree.Digit.one✝ a) = Lapis.VFS.FingerTree.Measurable.measure a
• Lapis.VFS.FingerTree.Digit.measure (Lapis.VFS.FingerTree.Digit.two✝ a a_1) = Lapis.VFS.FingerTree.Measurable.measure a + Lapis.VFS.FingerTree.Measurable.measure a_1

instance Lapis.VFS.FingerTree.instReprNode {α✝ : Type} [Repr α✝] : Repr (Lapis.VFS.FingerTree.Node✝ α✝)

Equations

• Lapis.VFS.FingerTree.instReprNode = { reprPrec := Lapis.VFS.FingerTree.instReprNode.repr }

def Lapis.VFS.FingerTree.instReprNode.repr {α✝ : Type} [Repr α✝] : Lapis.VFS.FingerTree.Node✝ α✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Lapis.VFS.FingerTree.instInhabitedNode.default {a✝ : Type} [Inhabited a✝] : Lapis.VFS.FingerTree.Node✝ a✝

Equations

• Lapis.VFS.FingerTree.instInhabitedNode.default = Lapis.VFS.FingerTree.Node.node2✝ default default default

instance Lapis.VFS.FingerTree.instInhabitedNode {a✝ : Type} [Inhabited a✝] : Inhabited (Lapis.VFS.FingerTree.Node✝ a✝)

Equations

• Lapis.VFS.FingerTree.instInhabitedNode = { default := Lapis.VFS.FingerTree.instInhabitedNode.default }

def Lapis.VFS.FingerTree.Node.measure {α : Type} : Lapis.VFS.FingerTree.Node✝ α → Measure

Equations

• Lapis.VFS.FingerTree.Node.measure (Lapis.VFS.FingerTree.Node.node2✝ a a_1 a_2) = a
• Lapis.VFS.FingerTree.Node.measure (Lapis.VFS.FingerTree.Node.node3✝ a a_1 a_2 a_3) = a

def Lapis.VFS.FingerTree.Node.toDigit {α : Type} : Lapis.VFS.FingerTree.Node✝ α → Lapis.VFS.FingerTree.Digit✝ α

Equations

• Lapis.VFS.FingerTree.Node.toDigit (Lapis.VFS.FingerTree.Node.node2✝ a a_1 a_2) = Lapis.VFS.FingerTree.Digit.two✝ a_1 a_2
• Lapis.VFS.FingerTree.Node.toDigit (Lapis.VFS.FingerTree.Node.node3✝ a a_1 a_2 a_3) = Lapis.VFS.FingerTree.Digit.three✝ a_1 a_2 a_3

def Lapis.VFS.FingerTree.Node.toList {α : Type} : Lapis.VFS.FingerTree.Node✝ α → List α

Equations

• Lapis.VFS.FingerTree.Node.toList (Lapis.VFS.FingerTree.Node.node2✝ a a_1 a_2) = [a_1, a_2]
• Lapis.VFS.FingerTree.Node.toList (Lapis.VFS.FingerTree.Node.node3✝ a a_1 a_2 a_3) = [a_1, a_2, a_3]

def Lapis.VFS.FingerTree.Node.mk2 {α : Type} [Measurable α] (a b : α) : Lapis.VFS.FingerTree.Node✝ α

Equations

• Lapis.VFS.FingerTree.Node.mk2 a b = Lapis.VFS.FingerTree.Node.node2✝ (Lapis.VFS.FingerTree.Measurable.measure a + Lapis.VFS.FingerTree.Measurable.measure b) a b

def Lapis.VFS.FingerTree.Node.mk3 {α : Type} [Measurable α] (a b c : α) : Lapis.VFS.FingerTree.Node✝ α

Equations

• One or more equations did not get rendered due to their size.

instance Lapis.VFS.FingerTree.instMeasurableNode {α : Type} : Measurable (Lapis.VFS.FingerTree.Node✝ α)

Nodes are themselves measurable via their cached measure

Equations

• Lapis.VFS.FingerTree.instMeasurableNode = { measure := Lapis.VFS.FingerTree.Node.measure }

instance Lapis.VFS.FingerTree.instInhabitedSpine {a✝ : Type} : Inhabited (Lapis.VFS.FingerTree.Spine✝ a✝)

Equations

• Lapis.VFS.FingerTree.instInhabitedSpine = { default := Lapis.VFS.FingerTree.instInhabitedSpine.default }

def Lapis.VFS.FingerTree.instInhabitedSpine.default {a✝ : Type} : Lapis.VFS.FingerTree.Spine✝ a✝

Equations

• Lapis.VFS.FingerTree.instInhabitedSpine.default = { nodes := default, cachedMeasure := default }

def Lapis.VFS.FingerTree.Spine.empty {α : Type} : Lapis.VFS.FingerTree.Spine✝ α

Equations

• Lapis.VFS.FingerTree.Spine.empty = { nodes := #[], cachedMeasure := Lapis.VFS.FingerTree.Measure.empty }

def Lapis.VFS.FingerTree.Spine.isEmpty {α : Type} (sp : Lapis.VFS.FingerTree.Spine✝ α) : Bool

Equations

• Lapis.VFS.FingerTree.Spine.isEmpty sp = (Lapis.VFS.FingerTree.Spine.nodes✝ sp).isEmpty

def Lapis.VFS.FingerTree.Spine.measure {α : Type} (sp : Lapis.VFS.FingerTree.Spine✝ α) : Measure

Equations

• Lapis.VFS.FingerTree.Spine.measure sp = Lapis.VFS.FingerTree.Spine.cachedMeasure✝ sp

def Lapis.VFS.FingerTree.Spine.single {α : Type} (n : Lapis.VFS.FingerTree.Node✝ α) : Lapis.VFS.FingerTree.Spine✝ α

Equations

• Lapis.VFS.FingerTree.Spine.single n = { nodes := #[n], cachedMeasure := Lapis.VFS.FingerTree.Node.measure n }

def Lapis.VFS.FingerTree.Spine.cons {α : Type} (n : Lapis.VFS.FingerTree.Node✝ α) (sp : Lapis.VFS.FingerTree.Spine✝ α) : Lapis.VFS.FingerTree.Spine✝¹ α

Equations

• One or more equations did not get rendered due to their size.

def Lapis.VFS.FingerTree.Spine.snoc {α : Type} (sp : Lapis.VFS.FingerTree.Spine✝ α) (n : Lapis.VFS.FingerTree.Node✝ α) : Lapis.VFS.FingerTree.Spine✝¹ α

Equations

• One or more equations did not get rendered due to their size.

def Lapis.VFS.FingerTree.Spine.viewL {α : Type} (sp : Lapis.VFS.FingerTree.Spine✝ α) : Option (Lapis.VFS.FingerTree.Node✝ α × Lapis.VFS.FingerTree.Spine✝¹ α)

Equations

• One or more equations did not get rendered due to their size.

def Lapis.VFS.FingerTree.Spine.viewR {α : Type} (sp : Lapis.VFS.FingerTree.Spine✝ α) : Option (Lapis.VFS.FingerTree.Spine✝¹ α × Lapis.VFS.FingerTree.Node✝ α)

Equations

• One or more equations did not get rendered due to their size.

def Lapis.VFS.FingerTree.Spine.append {α : Type} (sp1 sp2 : Lapis.VFS.FingerTree.Spine✝ α) : Lapis.VFS.FingerTree.Spine✝¹ α

Equations

• One or more equations did not get rendered due to their size.

def Lapis.VFS.FingerTree.Spine.fromArray {α : Type} (arr : Array (Lapis.VFS.FingerTree.Node✝ α)) : Lapis.VFS.FingerTree.Spine✝ α

Equations

• One or more equations did not get rendered due to their size.

def Lapis.VFS.FingerTree.Spine.toArray {α : Type} (sp : Lapis.VFS.FingerTree.Spine✝ α) : Array (Lapis.VFS.FingerTree.Node✝ α)

Equations

• Lapis.VFS.FingerTree.Spine.toArray sp = Lapis.VFS.FingerTree.Spine.nodes✝ sp

inductive Lapis.VFS.FingerTree.FingerTree (α : Type) : Type

A finger tree is either empty, a single element, or a deep tree

• empty {α : Type} : FingerTree α
• single {α : Type} : α → FingerTree α
• deep {α : Type} : Measure → Lapis.VFS.FingerTree.Digit✝ α → Lapis.VFS.FingerTree.Spine✝ α → Lapis.VFS.FingerTree.Digit✝¹ α → FingerTree α

instance Lapis.VFS.FingerTree.instInhabitedFingerTree {a✝ : Type} : Inhabited (FingerTree a✝)

Equations

• Lapis.VFS.FingerTree.instInhabitedFingerTree = { default := Lapis.VFS.FingerTree.instInhabitedFingerTree.default }

def Lapis.VFS.FingerTree.instInhabitedFingerTree.default {a✝ : Type} : FingerTree a✝

Equations

• Lapis.VFS.FingerTree.instInhabitedFingerTree.default = Lapis.VFS.FingerTree.FingerTree.empty

def Lapis.VFS.FingerTree.FingerTree.measure {α : Type} [Measurable α] : FingerTree α → Measure

Equations

• Lapis.VFS.FingerTree.FingerTree.empty.measure = Lapis.VFS.FingerTree.Measure.empty
• (Lapis.VFS.FingerTree.FingerTree.single a).measure = Lapis.VFS.FingerTree.Measurable.measure a
• (Lapis.VFS.FingerTree.FingerTree.deep m a a_1 a_2).measure = m

def Lapis.VFS.FingerTree.FingerTree.isEmpty {α : Type} : FingerTree α → Bool

Equations

• Lapis.VFS.FingerTree.FingerTree.empty.isEmpty = true
• x✝.isEmpty = false

def Lapis.VFS.FingerTree.FingerTree.mkDeep {α : Type} [Measurable α] (pr : Lapis.VFS.FingerTree.Digit✝ α) (sp : Lapis.VFS.FingerTree.Spine✝ α) (sf : Lapis.VFS.FingerTree.Digit✝¹ α) : FingerTree α

Equations

• One or more equations did not get rendered due to their size.

def Lapis.VFS.FingerTree.FingerTree.singleton {α : Type} (a : α) : FingerTree α

Equations

• Lapis.VFS.FingerTree.FingerTree.singleton a = Lapis.VFS.FingerTree.FingerTree.single a

def Lapis.VFS.FingerTree.FingerTree.cons {α : Type} [Measurable α] (a : α) (t : FingerTree α) : FingerTree α

Equations

• One or more equations did not get rendered due to their size.
• Lapis.VFS.FingerTree.FingerTree.cons a Lapis.VFS.FingerTree.FingerTree.empty = Lapis.VFS.FingerTree.FingerTree.single a

def Lapis.VFS.FingerTree.FingerTree.snoc {α : Type} [Measurable α] (t : FingerTree α) (a : α) : FingerTree α

Equations

• One or more equations did not get rendered due to their size.
• Lapis.VFS.FingerTree.FingerTree.empty.snoc a = Lapis.VFS.FingerTree.FingerTree.single a

inductive Lapis.VFS.FingerTree.FingerTree.ViewL (α : Type) : Type

• nil {α : Type} : ViewL α
• cons {α : Type} : α → FingerTree α → ViewL α

def Lapis.VFS.FingerTree.FingerTree.instInhabitedViewL.default {a✝ : Type} : ViewL a✝

Equations

• Lapis.VFS.FingerTree.FingerTree.instInhabitedViewL.default = Lapis.VFS.FingerTree.FingerTree.ViewL.nil

instance Lapis.VFS.FingerTree.FingerTree.instInhabitedViewL {a✝ : Type} : Inhabited (ViewL a✝)

Equations

• Lapis.VFS.FingerTree.FingerTree.instInhabitedViewL = { default := Lapis.VFS.FingerTree.FingerTree.instInhabitedViewL.default }

inductive Lapis.VFS.FingerTree.FingerTree.ViewR (α : Type) : Type

• nil {α : Type} : ViewR α
• snoc {α : Type} : FingerTree α → α → ViewR α

def Lapis.VFS.FingerTree.FingerTree.instInhabitedViewR.default {a✝ : Type} : ViewR a✝

Equations

• Lapis.VFS.FingerTree.FingerTree.instInhabitedViewR.default = Lapis.VFS.FingerTree.FingerTree.ViewR.nil

instance Lapis.VFS.FingerTree.FingerTree.instInhabitedViewR {a✝ : Type} : Inhabited (ViewR a✝)

Equations

• Lapis.VFS.FingerTree.FingerTree.instInhabitedViewR = { default := Lapis.VFS.FingerTree.FingerTree.instInhabitedViewR.default }

def Lapis.VFS.FingerTree.FingerTree.digitToTree {α : Type} [Measurable α] : Lapis.VFS.FingerTree.Digit✝ α → FingerTree α

Equations

• One or more equations did not get rendered due to their size.
• Lapis.VFS.FingerTree.FingerTree.digitToTree (Lapis.VFS.FingerTree.Digit.one✝ a) = Lapis.VFS.FingerTree.FingerTree.single a

def Lapis.VFS.FingerTree.FingerTree.viewL {α : Type} [Measurable α] (t : FingerTree α) : ViewL α

Equations

• One or more equations did not get rendered due to their size.
• Lapis.VFS.FingerTree.FingerTree.empty.viewL = Lapis.VFS.FingerTree.FingerTree.ViewL.nil
• (Lapis.VFS.FingerTree.FingerTree.single a).viewL = Lapis.VFS.FingerTree.FingerTree.ViewL.cons a Lapis.VFS.FingerTree.FingerTree.empty

def Lapis.VFS.FingerTree.FingerTree.viewR {α : Type} [Measurable α] (t : FingerTree α) : ViewR α

Equations

• One or more equations did not get rendered due to their size.
• Lapis.VFS.FingerTree.FingerTree.empty.viewR = Lapis.VFS.FingerTree.FingerTree.ViewR.nil
• (Lapis.VFS.FingerTree.FingerTree.single a).viewR = Lapis.VFS.FingerTree.FingerTree.ViewR.snoc Lapis.VFS.FingerTree.FingerTree.empty a

def Lapis.VFS.FingerTree.FingerTree.head? {α : Type} [Measurable α] (t : FingerTree α) : Option α

Equations

• t.head? = match t.viewL with | Lapis.VFS.FingerTree.FingerTree.ViewL.nil => none | Lapis.VFS.FingerTree.FingerTree.ViewL.cons a a_1 => some a

def Lapis.VFS.FingerTree.FingerTree.tail? {α : Type} [Measurable α] (t : FingerTree α) : Option (FingerTree α)

Equations

• t.tail? = match t.viewL with | Lapis.VFS.FingerTree.FingerTree.ViewL.nil => none | Lapis.VFS.FingerTree.FingerTree.ViewL.cons a rest => some rest

def Lapis.VFS.FingerTree.FingerTree.last? {α : Type} [Measurable α] (t : FingerTree α) : Option α

Equations

• t.last? = match t.viewR with | Lapis.VFS.FingerTree.FingerTree.ViewR.nil => none | Lapis.VFS.FingerTree.FingerTree.ViewR.snoc a a_1 => some a_1

def Lapis.VFS.FingerTree.FingerTree.init? {α : Type} [Measurable α] (t : FingerTree α) : Option (FingerTree α)

Equations

• t.init? = match t.viewR with | Lapis.VFS.FingerTree.FingerTree.ViewR.nil => none | Lapis.VFS.FingerTree.FingerTree.ViewR.snoc rest a => some rest

def Lapis.VFS.FingerTree.FingerTree.append3 {α : Type} [Measurable α] (t1 : FingerTree α) (mid : List α) (t2 : FingerTree α) : FingerTree α

Equations

• One or more equations did not get rendered due to their size.
• Lapis.VFS.FingerTree.FingerTree.empty.append3 mid t2 = Lapis.VFS.FingerTree.FingerTree.prependList✝ mid t2
• t1.append3 mid Lapis.VFS.FingerTree.FingerTree.empty = Lapis.VFS.FingerTree.FingerTree.appendList✝ t1 mid
• (Lapis.VFS.FingerTree.FingerTree.single a).append3 mid t2 = Lapis.VFS.FingerTree.FingerTree.cons a (Lapis.VFS.FingerTree.FingerTree.prependList✝ mid t2)
• t1.append3 mid (Lapis.VFS.FingerTree.FingerTree.single a) = (Lapis.VFS.FingerTree.FingerTree.appendList✝ t1 mid).snoc a

def Lapis.VFS.FingerTree.FingerTree.append {α : Type} [Measurable α] (t1 t2 : FingerTree α) : FingerTree α

Equations

• t1.append t2 = t1.append3 [] t2

instance Lapis.VFS.FingerTree.FingerTree.instAppendOfMeasurable {α : Type} [Measurable α] : Append (FingerTree α)

Equations

• Lapis.VFS.FingerTree.FingerTree.instAppendOfMeasurable = { append := Lapis.VFS.FingerTree.FingerTree.append }

structure Lapis.VFS.FingerTree.FingerTree.Split (α : Type) : Type

• left : FingerTree α
• pivot : α
• right : FingerTree α

def Lapis.VFS.FingerTree.FingerTree.instInhabitedSplit.default {a✝ : Type} [Inhabited a✝] : Split a✝

Equations

• Lapis.VFS.FingerTree.FingerTree.instInhabitedSplit.default = { left := default, pivot := default, right := default }

instance Lapis.VFS.FingerTree.FingerTree.instInhabitedSplit {a✝ : Type} [Inhabited a✝] : Inhabited (Split a✝)

Equations

• Lapis.VFS.FingerTree.FingerTree.instInhabitedSplit = { default := Lapis.VFS.FingerTree.FingerTree.instInhabitedSplit.default }

def Lapis.VFS.FingerTree.FingerTree.fromList {α : Type} [Measurable α] (l : List α) : FingerTree α

Equations

• Lapis.VFS.FingerTree.FingerTree.fromList l = List.foldl Lapis.VFS.FingerTree.FingerTree.snoc Lapis.VFS.FingerTree.FingerTree.empty l

def Lapis.VFS.FingerTree.FingerTree.fromArray {α : Type} [Measurable α] (arr : Array α) : FingerTree α

Equations

• Lapis.VFS.FingerTree.FingerTree.fromArray arr = Array.foldl Lapis.VFS.FingerTree.FingerTree.snoc Lapis.VFS.FingerTree.FingerTree.empty arr

def Lapis.VFS.FingerTree.FingerTree.split {α : Type} [Measurable α] [Inhabited α] (p : Measure → Bool) (t : FingerTree α) : Option (Split α)

Equations

• One or more equations did not get rendered due to their size.

def Lapis.VFS.FingerTree.FingerTree.splitAtBytes {α : Type} [Measurable α] [Inhabited α] (n : Nat) (t : FingerTree α) : Option (Split α)

Equations

• One or more equations did not get rendered due to their size.

def Lapis.VFS.FingerTree.FingerTree.splitAtLine {α : Type} [Measurable α] [Inhabited α] (n : Nat) (t : FingerTree α) : Option (Split α)

Equations

• One or more equations did not get rendered due to their size.

partial def Lapis.VFS.FingerTree.FingerTree.toList {α : Type} [Measurable α] (t : FingerTree α) : List α

def Lapis.VFS.FingerTree.FingerTree.toArray {α : Type} [Measurable α] (t : FingerTree α) : Array α

Equations

• t.toArray = Lapis.VFS.FingerTree.FingerTree.toArray.toArrayAux t #[]

partial def Lapis.VFS.FingerTree.FingerTree.toArray.toArrayAux {α : Type} [Measurable α] (t : FingerTree α) (acc : Array α) : Array α

def Lapis.VFS.FingerTree.FingerTree.foldl {α : Type} {β : Type u_1} [Measurable α] (f : β → α → β) (init : β) (t : FingerTree α) : β

Equations

• Lapis.VFS.FingerTree.FingerTree.foldl f init t = List.foldl f init t.toList

def Lapis.VFS.FingerTree.FingerTree.foldr {α : Type} {β : Type u_1} [Measurable α] (f : α → β → β) (init : β) (t : FingerTree α) : β

Equations

• Lapis.VFS.FingerTree.FingerTree.foldr f init t = List.foldr f init t.toList

def Lapis.VFS.FingerTree.FingerTree.size {α : Type} [Measurable α] (t : FingerTree α) : Nat

Equations

• One or more equations did not get rendered due to their size.
• Lapis.VFS.FingerTree.FingerTree.empty.size = 0
• (Lapis.VFS.FingerTree.FingerTree.single a).size = 1