Idris2Doc : Data.Nat.Views

Data.Nat.Views

Half : Nat -> Type
View for dividing a Nat in half
Totality: total
Constructors:
HalfOdd : (n : Nat) -> Half (S (n+n))
HalfEven : (n : Nat) -> Half (n+n)
HalfRec : Nat -> Type
View for dividing a Nat in half, recursively
Totality: total
Constructors:
HalfRecZ : HalfRecZ
HalfRecEven : (n : Nat) -> Lazy (HalfRecn) -> HalfRec (n+n)
HalfRecOdd : (n : Nat) -> Lazy (HalfRecn) -> HalfRec (S (n+n))
half : (n : Nat) -> Halfn
Covering function for the `Half` view
Totality: total
halfRec : (n : Nat) -> HalfRecn
Totality: total