Merge pull request #4481 from skibaa/patch-1
Make covering function public export
commit375d62f6719409206139bc56365773f383362e3b
authorNiklas Larsson <metaniklas@gmail.com>
dateTue 19 Jun 2018, 22:48 (8 years ago)
parenta272918a047bce
libs/base/Data/Nat/Views.idr+1−1
@@ -14,7 +14,7 @@ data HalfRec : Nat -> Type where
1414 HalfRecOdd : {n : Nat} -> (rec : Lazy (HalfRec n)) -> HalfRec (S (n + n))
1515
1616||| Covering function for the `Half` view
17−export
17+public export
1818half : (n : Nat) -> Half n
1919half Z = HalfEven {n=0}
2020half (S k) with (half k)