mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-24 06:52:19 +03:00
[ typo ] in test coverage007
This commit is contained in:
parent
1524b865c0
commit
9737f863a6
@ -27,4 +27,4 @@ badeq : (x : Nat) -> (y : Nat) -> (S (S x) = S y) -> Nat
|
||||
badeq x y p impossible
|
||||
|
||||
badeqL : (xs : List a) -> (ys : List a) -> (x :: xs = x :: y :: ys) -> Nat
|
||||
badeql xs ys p impossible
|
||||
badeqL xs ys p impossible
|
||||
|
@ -1,3 +1,3 @@
|
||||
1/1: Building eq (eq.idr)
|
||||
eq.idr:27:1--29:1:badeq x y p is not a valid impossible case
|
||||
eq.idr:30:1--31:1:No type declaration for Main.badeql
|
||||
eq.idr:30:1--31:1:badeqL xs ys p is not a valid impossible case
|
||||
|
Loading…
Reference in New Issue
Block a user