Make covering function public export
Without public export it's not evaluated well in REPL, see issue #4480
commita047bce64aac0c7554c9fb502e3f7581859e6c6d
authorAndrew Skiba <skibaa@gmail.com>
dateMon 18 Jun 2018, 17:32 (8 years ago)
parent88a9f38
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)