@@ -14,7 +14,7 @@ data HalfRec : Nat -> Type where
14 HalfRecOdd : {n : Nat} -> (rec : Lazy (HalfRec n)) -> HalfRec (S (n + n))
14 HalfRecOdd : {n : Nat} -> (rec : Lazy (HalfRec n)) -> HalfRec (S (n + n))
16||| Covering function for the `Half` view
16||| Covering function for the `Half` view
17−export
17+public export
18half : (n : Nat) -> Half n
18half : (n : Nat) -> Half n
19half Z = HalfEven {n=0}
19half Z = HalfEven {n=0}
20half (S k) with (half k)
20half (S k) with (half k)