mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-28 11:05:17 +03:00
3f914889b8
Can't export a type which refers to a private name. This has caught a couple of visibility errors in the libraries, code and tests, so they've been updated too.
28 lines
414 B
Idris
28 lines
414 B
Idris
infixr 5 ::
|
|
|
|
export
|
|
data List a = Nil | (::) a (List a)
|
|
export
|
|
data Nat = Z | S Nat
|
|
|
|
export
|
|
data Vect : Type -> Type where
|
|
export
|
|
data Set : Type -> Type where
|
|
|
|
namespace Vect
|
|
export
|
|
toList : Vect a -> List a
|
|
export
|
|
fromList : List a -> Vect a
|
|
|
|
namespace Set
|
|
export
|
|
toList : Set a -> List a
|
|
export
|
|
fromList : List a -> Set a
|
|
|
|
keepUnique : List b -> List b
|
|
keepUnique {b} xs = toList (fromList xs)
|
|
|