on aeb032a help sign in
Idris-dev/test/error008/error008.idr
5 lines 66 B history raw
1import Data.Vect
3s2 : x + sum Nil = x * fromInteger 0
4s2 = Refl