Skip to content

Commit f923c36

Browse files
committed
Please the linter again
1 parent 38bdbfb commit f923c36

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

tests/idris2/reg040/CoverBug.idr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ import Data.So
55
public export
66
data FastNat : Type where
77
MkFastNat : (val : Integer) -> {auto 0 prf : So True} -> FastNat
8-
8+
99
prv1 : Integer -> (x : Integer ** So $ True)
1010
prv1 x =
1111
case choose True of
@@ -16,6 +16,6 @@ fromInteger : Integer -> FastNat
1616
fromInteger v =
1717
let (v ** p) = prv1 $ v
1818
in MkFastNat v
19-
19+
2020
doit : FastNat -> FastNat
2121
doit 0 = 0

0 commit comments

Comments
 (0)