Data.Relation.Closure.ReflexiveTransitive

Definitions

data RTList : Rel a -> Rel a

Totality: total
Visibility: public export
Constructors:

Nil : RTList r x x

(::) : r x y -> RTList r y z -> RTList r x z

data SnocRTList : Rel a -> Rel a

Totality: total
Visibility: public export
Constructors:

Lin : SnocRTList r x x

(:<) : SnocRTList r x y -> r y z -> SnocRTList r x z

(<>>) : SnocRTList r x y -> RTList r y z -> RTList r x z

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 6

reflexive : (===) ~> RTList r

Totality: total
Visibility: export

(++) : RTList r x y -> RTList r y z -> RTList r x z

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

concat : RTList (RTList r) ~> RTList r

Totality: total
Visibility: export

gmap : (f : (a -> b)) -> p ~> (q `on` f) -> RTList p ~> (RTList q `on` f)

Totality: total
Visibility: export

map : p ~> q -> RTList p ~> RTList q

Totality: total
Visibility: export

reverseAcc : r ~> flip s -> flip (RTList s) x y -> RTList r y z -> flip (RTList s) x z

Totality: total
Visibility: export

reverse : r ~> flip s -> RTList r ~> flip (RTList s)

Totality: total
Visibility: export

deloop : (Ord a, DecEq a) => RTList r ~> RTList r

  Deloop detects whenever a proof forms a loop, and removes it e.g.
  
          x7 <-r- x6 <-r- x5
          |               ^
          r               r
          v               |
  x1 -r-> x2 -r-> x3 -r-> x4 -r-> x8
  
  becomes
  
  x1 -r-> x2 -r-> x3 -r-> x4 -r-> x8

Totality: total
Visibility: export