git.iko.soy/Idris-dev
on da672ec help sign in
Idris-dev/test/interactive001/expected
13 lines 332 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