Idris2Doc : Data.Nat.Views

Data.Nat.Views

dataHalf : 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)
dataHalfRec : Nat -> Type
  View for dividing a Nat in half, recursively

Totality: total
Constructors:
HalfRecZ : HalfRec0
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