git.iko.soy/Idris-dev
on 357cd83 help sign in
Idris-dev/test/test032/expected
12 lines 344 B history raw
1Type checking ./test032.idr
2isElem x [] = ?isElem_rhs_1
3isElem x (_ :: _) = ?isElem_rhs_3
5 localZipWith f (_ :: _) ys = ?localZipWith_rhs_1
6 localZipWith f (_ :: _) ys = ?localZipWith_rhs_2
8f x :: (map f xs)
9isElem2 x (y :: ys) with (_)
10 isElem2 x (y :: ys) | with_pat = ?isElem2_rhs
11 isElem3 x (x :: ys) | (Yes refl) = ?isElem3_rhs_3