TypeAligned.ZeroOne

Reflexive closure of a (binary) relation.  Internally used instead of Maybe, to maintain continuity of indexs.

Definitions

data ZeroOne : Rel a -> a -> a -> Type

  Reflexive closure of a relation

Totality: total
Visibility: public export
Constructors:

Zero : (0 _ : x = y) -> ZeroOne p x y

One : p x y -@ ZeroOne p x y

Hint: 

Reflexive a (ZeroOne p)

ZeroEq : ZeroOne p x x

  Convenience constructor

Totality: total
Visibility: export

singleton : p x y -> ZeroOne p x y

  Unrestricted 'One'

Totality: total
Visibility: export

mapReduceLOnce : {0 f : a -> b} -> {0 q : Rel b} -> p x y -@ q (f x) (f y) -> q (f x) (f x) -> ZeroOne p x y -@ q (f x) (f y)

  Linear 'mapReduceL'

Totality: total
Visibility: export

mapReduceROnce : {0 f : a -> b} -> {0 q : Rel b} -> p x y -@ q (f x) (f y) -> q (f y) (f y) -> ZeroOne p x y -@ q (f x) (f y)

  Linear 'mapReduceR'

Totality: total
Visibility: export

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

  Linear 'map'

Totality: total
Visibility: export

mapReduceL : {0 f : a -> b} -> {0 q : Rel b} -> (p x y -> q (f x) (f y)) -> q (f x) (f x) -> ZeroOne p x y -> q (f x) (f y)

  Reduce to left index, while changing relation

Totality: total
Visibility: export

mapReduceR : {0 f : a -> b} -> {0 q : Rel b} -> (p x y -> q (f x) (f y)) -> q (f y) (f y) -> ZeroOne p x y -> q (f x) (f y)

  Reduce to right index, while changing relation

Totality: total
Visibility: export

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

  Change inner relation

Totality: total
Visibility: export

reduceLOnce : p x x -> ZeroOne p x y -@ p x y

  Linear 'reduceL'

Totality: total
Visibility: export

reduceL : p x x -> ZeroOne p x y -> p x y

  Reduce to left index

Totality: total
Visibility: export

reduceROnce : p y y -> ZeroOne p x y -@ p x y

  Linear 'reduceR'

Totality: total
Visibility: export

reduceR : p y y -> ZeroOne p x y -> p x y

  Reduce to right index

Totality: total
Visibility: export