git.iko.soy/Idris-dev
on master help sign in
add %default total to Data/CoList.idr
576ff3dHeather
libs/contrib/Data/CoList.idr+1−1
compare with master
unifiedsplit
@@ -1,7 +1,7 @@
1module Data.CoList
1module Data.CoList
2
2
3%access public
3%access public
4−-- %default total
4+%default total
5
5
6||| Idris will know that it always can produce a new element in finite time
6||| Idris will know that it always can produce a new element in finite time
7codata CoList : Type -> Type where
7codata CoList : Type -> Type where