add %default total to Data/CoList.idr
commit576ff3d3d7ede80f7e13c77d3d4950b22710830f
authorHeather <heather@live.ru>
dateTue 28 Apr 2015, 16:13 (11 years ago)
parent4fba4e6
libs/contrib/Data/CoList.idr+1−1
@@ -1,7 +1,7 @@
11module Data.CoList
22
33%access public
4−-- %default total
4+%default total
55
66||| Idris will know that it always can produce a new element in finite time
77codata CoList : Type -> Type where