You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Sorry about the title, I'm not sure how to best title this bug
Steps to Reproduce
Foo.idr:
foo1 : List a -> List a -> List a
foo1 [] right = []
foo1 left [] = []
foo1 (x::xs) (y::ys) = []
empty1 : (left, right : List a) -> foo1 left right = []
empty1 [] right = Refl
empty1 left [] = ?hole1
empty1 (x::xs) (y::ys) = Refl
foo2 : List a -> List a -> List a
foo2 left [] = []
foo2 [] right = []
foo2 (x::xs) (y::ys) = []
empty2 : (left, right : List a) -> foo2 left right = []
empty2 [] right = ?hole2
empty2 left [] = Refl
empty2 (x::xs) (y::ys) = Refl
The difference between foo1 and foo2 is the order of the top two clauses.
Expected Behavior
$ idris2 Foo.idr
Foo> :t hole1
0 a : Type
left : List a
-------------------------------------
hole1 : [] = []
Foo> :t hole2
0 a : Type
right : List a
-------------------------------------
hole2 : [] = []
Observed Behavior
Foo> :t hole1
0 a : Type
left : List a
-------------------------------------
hole1 : (foo1 left []) = []
Foo> :t hole2
0 a : Type
right : List a
-------------------------------------
hole2 : (foo2 [] right) = []
Idris1 exhibits the same behaviour.
The text was updated successfully, but these errors were encountered:
The first two patterns are overlapping - foo [] [] matches both. If there's overlapping patterns, the clauses aren't definitional equalities, but instead the computational behaviour depends on the case trees that come out. It's certainly the case that foo1 left [] = [] for all left, but in general the normaliser isn't going to be able to spot this. So I probably can't do anything about this, I'm afraid.
Sorry about the title, I'm not sure how to best title this bug
Steps to Reproduce
Foo.idr
:The difference between
foo1
andfoo2
is the order of the top two clauses.Expected Behavior
Observed Behavior
Idris1 exhibits the same behaviour.
The text was updated successfully, but these errors were encountered: