git.iko.soy/Idris-dev
on ea65347 help sign in
Idris-dev/test/interactive001/expected
20 lines 473 B history raw
1isElem x [] = ?isElem_rhs_1
2isElem x (y :: xs) = ?isElem_rhs_3
4 localZipWith f (_ :: _) (x :: ys) = ?localZipWith_rhs_1
6f x :: map f xs
7isElem2 x (y :: ys) with (_)
8 isElem2 x (y :: ys) | with_pat = ?isElem2_rhs
10 isElem3 y (y :: ys) | (Yes Refl) = ?isElem3_rhs_3
12 [] => ?bar_1
13 (x :: ys) => ?bar_2
15elemVoid1 Here impossible
16elemVoid1 (There _) impossible
18 Here impossible
19 (There _) impossible