TypeAligned.TwoThree

Type primarily for internal usage holding either two or three relationships.
Used internally to provide fast append, even for when the meeting point is "ragged".

Reexports

Definitions

0 TwoThree : Rel a -> Rel a

  Utility type for 2-3 tree/list nesting

Totality: total
Visibility: public export

twice : p x y -@ (p y z -@ TwoThree p x z)

  Convenience constructor

Totality: total
Visibility: export

two : p x y -> p y z -> TwoThree p x z

  Convenience constructor, unrestricted

Totality: total
Visibility: export

thrice : p w x -@ (p x y -@ (p y z -@ TwoThree p w z))

  Convenience constructor

Totality: total
Visibility: export

three : p w x -> p x y -> p y z -> TwoThree p w z

  Convenience constructor, unrestricted

Totality: total
Visibility: export

0 .x : TwoThree p w z -> a

  Synthetic accessor; first (or only) meeting index

Totality: total
Visibility: export

0 .y : TwoThree p w z -> a

  Synthetic accessor; last (or only) meeting index

Totality: total
Visibility: export

.head : (tt : TwoThree p w z) -> p w (tt .x)

  Synthetic accessor

Totality: total
Visibility: export

head : (tt : TwoThree p w z) -> p w (tt .x)

  Synthetic accessor

Totality: total
Visibility: export

tail : (tt : TwoThree p w z) -> Sum p (Duo p) (tt .x) z

  Drop first relationship

Totality: total
Visibility: export

.last : (tt : TwoThree p w z) -> p (tt .y) z

  Synthetic accessor

Totality: total
Visibility: export

last : (tt : TwoThree p w z) -> p (tt .y) z

  Synthetic accessor

Totality: total
Visibility: export

init : (tt : TwoThree p w z) -> Sum p (Duo p) w (tt .y)

  Drop last relationship

Totality: total
Visibility: export

mapReduceOnce : {0 f : a -> b} -> {0 q : Rel b} -> p x y -@ q (f x) (f y) -> q x y -@ (q y z -@ q x z) -> TwoThree p x y -@ q (f x) (f y)

  Reduce while changing inner relation

Totality: total
Visibility: export

mapOnce : {0 f : a -> b} -> p x y -@ q (f x) (f y) -> TwoThree p x y -@ TwoThree q (f x) (f y)

  Linear 'map'

Totality: total
Visibility: export

mapReduce : {0 f : a -> b} -> {0 q : Rel b} -> (p x y -> q (f x) (f y)) -> (q x y -> q y z -> q x z) -> TwoThree p x y -> q (f x) (f y)

  Reduce while changing inner relation

Totality: total
Visibility: export

map : {0 f : a -> b} -> (p x y -> q (f x) (f y)) -> TwoThree p x y -> TwoThree q (f x) (f y)

  Change inner relation

Totality: total
Visibility: export

reduceOnce : p x y -@ (p y z -@ p x z) -> TwoThree p x y -@ p x y

  Linear 'reduce'

Totality: total
Visibility: export

reduce : (p x y -> p y z -> p x z) -> TwoThree p x y -> p x y

  Reduce to inner relation

Totality: total
Visibility: export