git.iko.soy/Idris-dev
on 02de034 help sign in
Idris-dev/test/interactive001/expected
14 lines 360 B history raw
1Type checking ./test032.idr
2isElem x [] = ?isElem_rhs_1
3isElem x (y :: xs) = ?isElem_rhs_3
5 localZipWith f (_ :: _) (x :: ys) = ?localZipWith_rhs_1
7f x :: map f xs
8isElem2 x (y :: ys) with (_)
9 isElem2 x (y :: ys) | with_pat = ?isElem2_rhs
10 isElem3 x (x :: ys) | (Yes Refl) = ?isElem3_rhs_3
12 [] => ?bar_1
13 (x :: ys) => ?bar_2