git.iko.soy/Idris-dev
on aa062fc help sign in
Idris-dev/test/interactive001/expected
19 lines 466 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
9 isElem3 x (x :: ys) | (Yes Refl) = ?isElem3_rhs_3
11 [] => ?bar_1
12 (x :: ys) => ?bar_2
14elemVoid1 Here impossible
15elemVoid1 (There _) impossible
17 Here impossible
18 (There _) impossible