FuPy logo

Prelude: Natural number and (in)finite lists

Further convenience functions and types

Among others:

  • swap[A, B]: Func[Both[A, B], Both[B, A]] (swap components of tuple: swap(a, b) = (b, a))

  • coswap[A, B]: Func[Either[A, B], Either[B, A]] (swap left/right injection: coswap(left(a)) = right(a) and coswap(right(b)) = left(b))

To Be Completed

The (co)inductive type of natural numbers: Nat

To Be Completed

The (co)inductive type of lists: List_

To Be Completed

Treating int (>=0) and list as inductive types

To Be Completed