Merge pull request #4897 from SekiT/fix-typo-erase

Fix typo: erae => erase
idris-lang · Jun 26, 2021 · 2ef8238 · 2ef8238
2 parents a13caeb + 12ad2f4
commit 2ef8238
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/libs/base/Data/List/Views.idr b/libs/base/Data/List/Views.idr
@@ -28,7 +28,7 @@ public export
 data Split : List a -> Type where
      SplitNil : Split []
      SplitOne : Split [x]
-     SplitPair : {x, y : a} -> {xs, ys : List a} -> -- Explicit, don't erae
+     SplitPair : {x, y : a} -> {xs, ys : List a} -> -- Explicit, don't erase
                  Split (x :: xs ++ y :: ys)
 
 splitHelp : (head : a) ->