on aeb032a help sign in
Idris-dev/test/error008/error008a.idr
5 lines 93 B history raw
1import Data.Vect
3s1 : Num a => {x : a} -> x + sum {a} Nil = x -- * fromInteger 0
4s1 = Refl