Skip to content

Commit 12ad2f4

Browse files
authored
Fix typo: erae => erase
1 parent a13caeb commit 12ad2f4

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

libs/base/Data/List/Views.idr

+1-1
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ public export
2828
data Split : List a -> Type where
2929
SplitNil : Split []
3030
SplitOne : Split [x]
31-
SplitPair : {x, y : a} -> {xs, ys : List a} -> -- Explicit, don't erae
31+
SplitPair : {x, y : a} -> {xs, ys : List a} -> -- Explicit, don't erase
3232
Split (x :: xs ++ y :: ys)
3333

3434
splitHelp : (head : a) ->

0 commit comments

Comments
 (0)