Skip to content

Commit 30d8a0b

Browse files
WalkerCodeRangerdavidfstr
authored andcommitted
Update to compile under Idris v1
1 parent 136cb0f commit 30d8a0b

File tree

1 file changed

+1
-2
lines changed

1 file changed

+1
-2
lines changed

InsertionSort.idr

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -60,9 +60,8 @@ chooseLte x y =
6060
-- IsSorted
6161

6262
-- Proof that `xs` is sorted.
63-
data IsSorted : Ord e => (xs:Vect n e) -> Type where
63+
data IsSorted : (xs:Vect n e) -> Type where
6464
IsSortedZero :
65-
Ord e =>
6665
IsSorted Nil
6766
IsSortedOne :
6867
Ord e =>

0 commit comments

Comments
 (0)