0 | module Data.Linear.LList
 1 |
 2 | import Data.Linear.Bifunctor
 3 | import Data.Linear.Interface
 4 | import Data.Linear.Notation
 5 | import Data.Linear.LNat
 6 |
 7 | %default total
 8 |
 9 | public export
10 | data LList : Type -> Type where
11 |   Nil : LList a
12 |   (::) : a -@ LList a -@ LList a
13 |
14 | %name LList xs, ys, zs, ws
15 |
16 | export
17 | length : Consumable a => LList a -@ LNat
18 | length [] = Zero
19 | length (x :: xs) = consume x `seq` length xs
20 |
21 | export
22 | Consumable a => Consumable (LList a) where
23 |   consume [] = ()
24 |   consume (x :: xs) = x `seq` consume xs
25 |
26 | export
27 | Duplicable a => Duplicable (LList a) where
28 |   duplicate [] = [[], []]
29 |   duplicate (x :: xs) = (::) <$> duplicate x <*> duplicate xs
30 |