Data.Nat.Views

Definitions

data Half : Nat -> Type

  View for dividing a Nat in half

Totality: total
Visibility: public export
Constructors:

HalfOdd : (n : Nat) -> Half (S (n + n))

HalfEven : (n : Nat) -> Half (n + n)

data HalfRec : Nat -> Type

  View for dividing a Nat in half, recursively

Totality: total
Visibility: public export
Constructors:

HalfRecZ : HalfRec 0

HalfRecEven : (n : Nat) -> Lazy (HalfRec n) -> HalfRec (n + n)

HalfRecOdd : (n : Nat) -> Lazy (HalfRec n) -> HalfRec (S (n + n))

half : (n : Nat) -> Half n

  Covering function for the `Half` view

Totality: total
Visibility: public export

halfRec : (n : Nat) -> HalfRec n

Totality: total
Visibility: public export