- data 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)
- data HalfRec : Nat -> Type
View for dividing a Nat in half, recursively
Totality: total
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- halfRec : (n : Nat) -> HalfRec n
- Totality: total