{"header":{"message":"Split Data.LinkedList","description":null,"timestamp":"2021-06-19T21:45:57.895283559Z","authors":[{"email":"fabianhjr@protonmail.com","full_name":"Fabián Heredia Montiel","name":"fabian"}]},"hash":"BJGJCKMBY65UJSUP4DGEQVR2DZAXWDJKRVOGGTKQDQ4XAMBRLRZAC","authors":[],"deps":{"hashes":[["BJGJCKMBY65UJSUP4DGEQVR2DZAXWDJKRVOGGTKQDQ4XAMBRLRZAC","Split Data.LinkedList"],["AA",null],["4L2YWRMCKZ56NCRC44XVDZQ5BEKHX26C4GQZ5TIL35Y33VKFTBCQC","Semigroup Natural"],["YE3EAD3XYKXRHEJN4VLBVBQM2EISKFHAESPOZ6S4QMLA6YZEVDQQC","Fix `Equiv` signatures to take into account multiple implementations of interface"],["K7TT3LDM6HYYXLSYFSJZRQZ6GOGTDJ7F5KFU7GBPJOKN2DHJLHMQC","Add `Data.LinkedList`"],["PUFI27GBQLTD64UCR35JZOWINUF2A5BWFUI5G6ZQN3UFQZPZB54AC","Implement `Data.LinkedList` `Applicative` (Mostly)"],["4WZ2PYVOKVZFB6Q44LR6APOSMZTUR566HI5IOFLDCA5C7RQRMFRAC","Add `Data.LinkedList` `Monad` Instance"],["ZJMXCVWEW2XHBZGNQUHTW7JRIAEAE5UDTASSD75WJG55MDOUZ3MAC","Implement `LinkedList`'s `Monoid` interface"],["NYMIFK2WBHU4G34QF4GZP63ATL2EQC6PLAQLWZMUTPDGDPQUEKVQC","Make a HelloWorld sample work"],["RUIGRXTKM6BQ532W7KU3RKDXMRNRGDVGMA2ODMX2D2F3PCLF3GAQC","Refactor"],["4KXMGXQ6PTWVMINMKRCQE7DIJXUYMO7SVNR6AQ243QULY7IZLUYAC","Refactor Algebra"],["XNPLRKJ4ZK442XNJ5BC7TO3DKXGXFSOSGBZBPW5HZZDHY3IVD6FAC","Init"],["CO3C7GSZ2X62ALXW2EAWDHCRSXCNVKIIHCL47GYZ32OHZER4NLZQC","Create Data.Either"]],"deps":["4L2YWRMCKZ56NCRC44XVDZQ5BEKHX26C4GQZ5TIL35Y33VKFTBCQC"],"known":["K7TT3LDM6HYYXLSYFSJZRQZ6GOGTDJ7F5KFU7GBPJOKN2DHJLHMQC","YE3EAD3XYKXRHEJN4VLBVBQM2EISKFHAESPOZ6S4QMLA6YZEVDQQC","ZJMXCVWEW2XHBZGNQUHTW7JRIAEAE5UDTASSD75WJG55MDOUZ3MAC","PUFI27GBQLTD64UCR35JZOWINUF2A5BWFUI5G6ZQN3UFQZPZB54AC","4WZ2PYVOKVZFB6Q44LR6APOSMZTUR566HI5IOFLDCA5C7RQRMFRAC","4KXMGXQ6PTWVMINMKRCQE7DIJXUYMO7SVNR6AQ243QULY7IZLUYAC","NYMIFK2WBHU4G34QF4GZP63ATL2EQC6PLAQLWZMUTPDGDPQUEKVQC","RUIGRXTKM6BQ532W7KU3RKDXMRNRGDVGMA2ODMX2D2F3PCLF3GAQC"]},"hunks":[{"Edit":{"inode":{"change":12,"pos":6174},"path":"veribase.ipkg","line":39,"atom":{"NewVertex":{"up_context":[{"change":13,"pos":1314}],"down_context":[{"change":3,"pos":2042}],"flag":"BLOCK","start":0,"end":165,"inode":{"change":12,"pos":6174}}},"contents":[{"Add":""},{"Add":"\t, Data.LinkedList.Applicative"},{"Add":"\t, Data.LinkedList.Basic"},{"Add":"\t, Data.LinkedList.Equivalence"},{"Add":"\t, Data.LinkedList.Functor"},{"Add":"\t, Data.LinkedList.Group"},{"Add":"\t, Data.LinkedList.Monad"}]}},{"Edit":{"inode":{"change":3,"pos":17},"path":"src/Data/LinkedList.idr","line":2,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":41},"to":{"change":3,"start":41,"end":57},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":57},"to":{"change":3,"start":445,"end":482},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":482},"to":{"change":3,"start":57,"end":58},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":57},"to":{"change":3,"start":57,"end":58},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":823},"to":{"change":3,"start":823,"end":854},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":854},"to":{"change":3,"start":448,"end":483},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":483},"to":{"change":3,"start":854,"end":883},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":854},"to":{"change":3,"start":854,"end":883},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":883},"to":{"change":3,"start":483,"end":511},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":511},"to":{"change":3,"start":484,"end":515},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":511},"to":{"change":3,"start":883,"end":911},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":515},"to":{"change":3,"start":883,"end":911},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":883},"to":{"change":3,"start":883,"end":911},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":22},"to":{"change":3,"start":108,"end":201},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":543},"to":{"change":3,"start":108,"end":201},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":911},"to":{"change":3,"start":108,"end":201},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":108},"to":{"change":3,"start":108,"end":201},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":201},"to":{"change":3,"start":0,"end":222},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":222},"to":{"change":3,"start":372,"end":441},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":372},"to":{"change":3,"start":372,"end":441},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":441},"to":{"change":3,"start":223,"end":284},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":284},"to":{"change":3,"start":497,"end":512},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":497},"to":{"change":3,"start":497,"end":512},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":512},"to":{"change":3,"start":285,"end":362},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":362},"to":{"change":3,"start":561,"end":659},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":561},"to":{"change":3,"start":561,"end":659},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":659},"to":{"change":3,"start":363,"end":440},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":440},"to":{"change":3,"start":708,"end":806},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":708},"to":{"change":3,"start":708,"end":806},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":806},"to":{"change":3,"start":441,"end":584},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":963},"to":{"change":3,"start":585,"end":641},"introduced_by":3}],"inode":{"change":3,"pos":17}}},"contents":[{"Del":"\nimport Builtin\n"},{"Del":"\nimport Algebra.Relation.Equivalence\n"},{"Del":"\n"},{"Del":"import Algebra.Control.Functor\n"},{"Del":"import Algebra.Control.Applicative\n"},{"Del":"import Algebra.Control.Monad\n"},{"Del":"\nimport Algebra.Group.Magma\n"},{"Del":"import Algebra.Group.Semigroup\n"},{"Del":"import Algebra.Group.Monoid\n"},{"Del":"\n%default total\n\ninfixr 7 ::\n\npublic export\ndata LinkedList t = Nil | (::) t (LinkedList t)\n\n"},{"Del":"data LinkedListEquiv : Equivalence t => (a, b : LinkedList t) -> Type where\n BothEmpty : (e : Equivalence t) => LinkedListEquiv @{e} Nil Nil\n EquivHeadAndTail : (e : Equivalence t) => {a, b : t} -> {x, y : LinkedList t}\n"},{"Del":" -> (ok1: Equiv a b) -> (ok2: LinkedListEquiv x y)\n"},{"Del":" -> LinkedListEquiv @{e} (a :: x) (b :: y)\n"},{"Del":"\npublic export\n"},{"Del":"(e : Equivalence a) => Uninhabited (LinkedListEquiv @{e} Nil (h :: t)) where\n"},{"Del":" uninhabited BothEmpty impossible\n uninhabited (EquivHeadAndTail h t) impossible\n\npublic export\n"},{"Del":"(e : Equivalence a) => Uninhabited (LinkedListEquiv @{e} (h :: t) Nil) where\n"},{"Del":" uninhabited BothEmpty impossible\n uninhabited (EquivHeadAndTail h t) impossible\n\npublic export\n"},{"Del":"fromNotEquivHead : (e : Equivalence t) => {a, b : t} -> (ok: Not (Equiv a b))\n -> Not (LinkedListEquiv @{e} (a :: x) (b :: y))\n"},{"Del":"fromNotEquivHead ctr (EquivHeadAndTail prf _) = ctr prf\n"}]}},{"Replacement":{"inode":{"change":3,"pos":17},"path":"src/Data/LinkedList.idr","line":3,"ins":{"up_context":[{"change":3,"pos":1018}],"down_context":[{"change":3,"pos":1315}],"flag":"BLOCK","start":166,"end":202,"inode":{"change":3,"pos":17}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1018},"to":{"change":3,"start":1018,"end":1032},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1032},"to":{"change":3,"start":642,"end":786},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1168},"to":{"change":3,"start":1168,"end":1224},"introduced_by":3}],"inode":{"change":3,"pos":17}},"ins_contents":[{"Add":"import public Data.LinkedList.Basic"}],"del_contents":[{"Del":"public export\n"},{"Del":"fromNotEquivTail : (e : Equivalence t) => (ok: Not (LinkedListEquiv @{e} x y))\n -> Not (LinkedListEquiv @{e} (a :: x) (b :: y))\n"},{"Del":"fromNotEquivTail ctr (EquivHeadAndTail _ prf) = ctr prf\n"}]}},{"Replacement":{"inode":{"change":3,"pos":17},"path":"src/Data/LinkedList.idr","line":5,"ins":{"up_context":[{"change":3,"pos":1316}],"down_context":[{"change":3,"pos":1261}],"flag":"BLOCK","start":203,"end":245,"inode":{"change":3,"pos":17}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1316},"to":{"change":3,"start":787,"end":887},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":887},"to":{"change":3,"start":516,"end":687},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":687},"to":{"change":3,"start":1087,"end":1145},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1087},"to":{"change":3,"start":1087,"end":1145},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":1145},"to":{"change":3,"start":1505,"end":1566},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1505},"to":{"change":3,"start":1505,"end":1566},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1566},"to":{"change":3,"start":1146,"end":1261},"introduced_by":3}],"inode":{"change":3,"pos":17}},"ins_contents":[{"Add":"import public Data.LinkedList.Equivalence"}],"del_contents":[{"Del":"decLinkedListEquiv : (e : Equivalence t) => (a, b : LinkedList t) -> Dec (LinkedListEquiv @{e} a b)\n"},{"Del":"decLinkedListEquiv Nil Nil = Yes BothEmpty\ndecLinkedListEquiv Nil (_::_) = No absurd\ndecLinkedListEquiv (_::_) Nil = No absurd\ndecLinkedListEquiv @{e} (h1::t1) (h2::t2) =\n"},{"Del":" case (decEquiv @{e} h1 h2, decLinkedListEquiv t1 t2) of\n"},{"Del":" (Yes prf1, Yes prf2) => Yes $ EquivHeadAndTail prf1 prf2\n"},{"Del":" (Yes prf1, No ctra2) => No $ fromNotEquivTail @{e} ctra2\n (No ctra1, _) => No $ fromNotEquivHead @{e} ctra1\n"}]}},{"Replacement":{"inode":{"change":3,"pos":17},"path":"src/Data/LinkedList.idr","line":7,"ins":{"up_context":[{"change":3,"pos":1262}],"down_context":[{"change":3,"pos":149}],"flag":"BLOCK","start":246,"end":282,"inode":{"change":3,"pos":17}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1262},"to":{"change":3,"start":1262,"end":1389},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1389},"to":{"change":3,"start":23,"end":149},"introduced_by":3}],"inode":{"change":3,"pos":17}},"ins_contents":[{"Add":"import public Data.LinkedList.Group"}],"del_contents":[{"Del":"public export\n(Equivalence t) => Equivalence (LinkedList t) where\n Equiv = LinkedListEquiv\n decEquiv = decLinkedListEquiv\n"},{"Del":"\npublic export\nconcat : LinkedList t -> LinkedList t -> LinkedList t\nconcat Nil y = y\nconcat (x::xs) y = x :: concat xs y\n"}]}},{"Replacement":{"inode":{"change":3,"pos":17},"path":"src/Data/LinkedList.idr","line":9,"ins":{"up_context":[{"change":3,"pos":150}],"down_context":[],"flag":"BLOCK","start":283,"end":399,"inode":{"change":3,"pos":17}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":150},"to":{"change":3,"start":150,"end":389},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":389},"to":{"change":2,"start":1838,"end":1949},"introduced_by":2},{"previous":"","flag":"DELETED","from":{"change":3,"pos":506},"to":{"change":3,"start":1718,"end":1733},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":1389},"to":{"change":3,"start":1718,"end":1733},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":2,"pos":1949},"to":{"change":3,"start":1718,"end":1733},"introduced_by":2},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1718},"to":{"change":3,"start":1718,"end":1733},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1733},"to":{"change":3,"start":507,"end":582},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":582},"to":{"change":3,"start":22,"end":96},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":96},"to":{"change":3,"start":649,"end":686},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":649},"to":{"change":3,"start":649,"end":686},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":686},"to":{"change":3,"start":97,"end":173},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":173},"to":{"change":3,"start":755,"end":770},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":755},"to":{"change":3,"start":755,"end":770},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":770},"to":{"change":3,"start":1733,"end":1758},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1733},"to":{"change":3,"start":1733,"end":1758},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1758},"to":{"change":3,"start":688,"end":738},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":738},"to":{"change":3,"start":1808,"end":1836},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1808},"to":{"change":3,"start":1808,"end":1836},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1836},"to":{"change":3,"start":739,"end":838},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":838},"to":{"change":3,"start":1935,"end":1936},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1935},"to":{"change":3,"start":1935,"end":1936},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1936},"to":{"change":3,"start":839,"end":947},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":947},"to":{"change":3,"start":28,"end":121},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2041},"to":{"change":3,"start":28,"end":121},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":121},"to":{"change":3,"start":948,"end":986},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":986},"to":{"change":3,"start":157,"end":294},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":157},"to":{"change":3,"start":157,"end":294},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":302},"to":{"change":3,"start":302,"end":493},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":493},"to":{"change":3,"start":987,"end":1032},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":1032},"to":{"change":3,"start":538,"end":795},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":538},"to":{"change":3,"start":538,"end":795},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":795},"to":{"change":3,"start":1033,"end":1074},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":1074},"to":{"change":3,"start":836,"end":892},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":836},"to":{"change":3,"start":836,"end":892},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":892},"to":{"change":3,"start":1075,"end":1116},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":1116},"to":{"change":3,"start":892,"end":914},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":892},"to":{"change":3,"start":892,"end":914},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":914},"to":{"change":3,"start":174,"end":212},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":212},"to":{"change":3,"start":544,"end":598},"introduced_by":3},{"previous":"","flag":"DELETED","from":{"change":3,"pos":598},"to":{"change":3,"start":271,"end":486},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":271},"to":{"change":3,"start":271,"end":486},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":486},"to":{"change":2,"start":1950,"end":2169},"introduced_by":2}],"inode":{"change":3,"pos":17}},"ins_contents":[{"Add":"import public Data.LinkedList.Functor"},{"Add":"import public Data.LinkedList.Applicative"},{"Add":"import public Data.LinkedList.Monad"}],"del_contents":[{"Del":"public export\nconcatNil : (l : LinkedList t) -> concat l Nil = l\nconcatNil Nil = Refl\nconcatNil (x::xs) = rewrite concatNil xs in Refl\n\npublic export\nMagma (LinkedList t) where\n (<>) = concat\n\npublic export\nSemigroup (LinkedList t) where\n"},{"Del":" proofAssociative Nil _ _ = Refl\n proofAssociative (x::xs) y z = rewrite proofAssociative xs y z in Refl\n"},{"Del":"\npublic export\n"},{"Del":"Monoid (LinkedList t) where\n id = Nil\n\n proofLeftIdentity Nil = Refl\n"},{"Del":" proofLeftIdentity (x::xs) = rewrite Monoid.proofLeftIdentity xs in Refl\n"},{"Del":"\n proofRightIdentity Nil = Refl\n"},{"Del":" proofRightIdentity (y::ys) = rewrite Monoid.proofRightIdentity ys in Refl\n"},{"Del":"\npublic export\n"},{"Del":"Functor LinkedList where\n"},{"Del":" _ <$> Nil = Nil\n f <$> (h::t) = f h :: f <$> t\n"},{"Del":"\n proofIdentity Nil = Refl\n"},{"Del":" proofIdentity (_::t) with (proofIdentity t)\n proofIdentity (_::_) | prf = rewrite prf in Refl\n"},{"Del":"\n"},{"Del":" proofComposition f g Nil = Refl\n proofComposition f g (_::t) = rewrite proofComposition f g t in Refl\n"},{"Del":"\npublic export\napp : LinkedList (a -> b) -> LinkedList a -> LinkedList b\napp Nil _ = Nil\n"},{"Del":"app (f::fs) l = (f <$> l) <> app fs l\n"},{"Del":"\npublic export\nappNil : (f : LinkedList (a -> b)) -> f `app` Nil = Nil\nappNil Nil = Refl\nappNil (f::fs) = rewrite appNil fs in Refl\n\n"},{"Del":"public export\nApplicative LinkedList where\n pure x = [x]\n\n (<*>) = app\n\n proofIdentity Nil = Refl\n proofIdentity (_::xs) with (Functor.proofIdentity xs)\n proofIdentity (_::xs) | prf =\n"},{"Del":" rewrite concatNil (identity <$> xs) in\n"},{"Del":" rewrite prf in Refl\n\n proofHomomorphism f x = Refl\n\n proofInterchange Nil x = Refl\n proofInterchange (f::fs) x = rewrite proofInterchange fs x in Refl\n\n proofComposition Nil Nil _ = Refl\n proofComposition Nil (_::gs) _ =\n rewrite appNil gs in\n"},{"Del":" -- rewrite concatNil ((.) <$> gs) in\n"},{"Del":" ?holeComposition1\n proofComposition (f::fs) gs _ =\n"},{"Del":" -- rewrite concatNil ((.) <$> gs) in\n"},{"Del":" ?holeComposition2\n"},{"Del":"\npublic export\nMonad LinkedList where\n"},{"Del":" Nil >>= _ = Nil\n (x::xs) >>= f = f x <> (xs >>= f)\n"},{"Del":"\n proofLeftIdentity x f = rewrite concatNil (f x) in Refl\n\n proofRightIdentity Nil = Refl\n proofRightIdentity (x::xs) with (Monad.proofRightIdentity xs)\n proofRightIdentity (_::_) | prf = rewrite prf in Refl\n\n"},{"Del":" proofAssociative Nil f g = Refl\n proofAssociative (x::xs) f g with (f x)\n proofAssociative (x::xs) f g | Nil = rewrite proofAssociative xs f g in Refl\n proofAssociative (x::xs) f g | (r::rs) = ?holeAssociative\n"}]}},{"FileAdd":{"meta":{"basename":"LinkedList","metadata":576},"context":[{"change":12,"pos":14}],"contents":[]}},{"FileAdd":{"meta":{"basename":"Monad.idr","metadata":0},"context":[{"change":0,"pos":413}],"contents":[{"Add":"module Data.LinkedList.Monad"},{"Add":""},{"Add":"import Builtin"},{"Add":""},{"Add":"import Algebra.Control.Applicative"},{"Add":"import Algebra.Control.Monad"},{"Add":""},{"Add":"import public Data.LinkedList.Basic"},{"Add":"import public Data.LinkedList.Applicative"},{"Add":""},{"Add":"public export"},{"Add":"Monad LinkedList where"},{"Add":" Nil >>= _ = Nil"},{"Add":" (x::xs) >>= f = f x `concat` (xs >>= f)"},{"Add":""},{"Add":" proofLeftIdentity x f = rewrite proofConcatRightIdentity (f x) in Refl"},{"Add":""},{"Add":" proofRightIdentity Nil = Refl"},{"Add":" proofRightIdentity (x::xs) with (Monad.proofRightIdentity xs)"},{"Add":" proofRightIdentity (_::_) | prf = rewrite prf in Refl"},{"Add":""},{"Add":" proofAssociative Nil f g = Refl"},{"Add":" proofAssociative (x::xs) f g = case f x of"},{"Add":" Nil => ?holeAssociative1"},{"Add":" (r::rs) => ?holeAssociative2"}]}},{"FileAdd":{"meta":{"basename":"Group.idr","metadata":0},"context":[{"change":0,"pos":413}],"contents":[{"Add":"module Data.LinkedList.Group"},{"Add":""},{"Add":"import Builtin"},{"Add":""},{"Add":"import Algebra.Group.Magma"},{"Add":"import Algebra.Group.Semigroup"},{"Add":"import Algebra.Group.Monoid"},{"Add":""},{"Add":"import public Data.LinkedList.Basic"},{"Add":""},{"Add":"%default total"},{"Add":""},{"Add":"public export"},{"Add":"Magma (LinkedList t) where"},{"Add":" (<>) = concat"},{"Add":""},{"Add":"public export"},{"Add":"Semigroup (LinkedList t) where"},{"Add":" proofAssociative Nil _ _ = Refl"},{"Add":" proofAssociative (x::xs) y z = rewrite proofAssociative xs y z in Refl"},{"Add":""},{"Add":"public export"},{"Add":"Monoid (LinkedList t) where"},{"Add":" id = Nil"},{"Add":""},{"Add":" proofLeftIdentity Nil = Refl"},{"Add":" proofLeftIdentity (x::xs) = rewrite Monoid.proofLeftIdentity xs in Refl"},{"Add":""},{"Add":" proofRightIdentity Nil = Refl"},{"Add":" proofRightIdentity (y::ys) = rewrite Monoid.proofRightIdentity ys in Refl"}]}},{"FileAdd":{"meta":{"basename":"Functor.idr","metadata":0},"context":[{"change":0,"pos":413}],"contents":[{"Add":"module Data.LinkedList.Functor"},{"Add":""},{"Add":"import Builtin"},{"Add":""},{"Add":"import Algebra.Control.Functor"},{"Add":""},{"Add":"import public Data.LinkedList.Basic"},{"Add":""},{"Add":"public export"},{"Add":"Functor LinkedList where"},{"Add":" _ <$> Nil = Nil"},{"Add":" f <$> (h::t) = f h :: f <$> t"},{"Add":""},{"Add":" proofIdentity Nil = Refl"},{"Add":" proofIdentity (_::t) with (proofIdentity t)"},{"Add":" proofIdentity (_::_) | prf = rewrite prf in Refl"},{"Add":""},{"Add":" proofComposition f g Nil = Refl"},{"Add":" proofComposition f g (_::t) = rewrite proofComposition f g t in Refl"}]}},{"FileAdd":{"meta":{"basename":"Equivalence.idr","metadata":0},"context":[{"change":0,"pos":413}],"contents":[{"Add":"module Data.LinkedList.Equivalence"},{"Add":""},{"Add":"import Builtin"},{"Add":""},{"Add":"import Algebra.Relation.Equivalence"},{"Add":""},{"Add":"import public Data.LinkedList.Basic"},{"Add":""},{"Add":"%default total"},{"Add":""},{"Add":"public export"},{"Add":"data LinkedListEquiv : Equivalence t => (a, b : LinkedList t) -> Type where"},{"Add":" BothEmpty : (e : Equivalence t) => LinkedListEquiv @{e} Nil Nil"},{"Add":" EquivHeadAndTail : (e : Equivalence t) => {a, b : t} -> {x, y : LinkedList t}"},{"Add":" -> (ok1: Equiv a b) -> (ok2: LinkedListEquiv x y)"},{"Add":" -> LinkedListEquiv @{e} (a :: x) (b :: y)"},{"Add":""},{"Add":"public export"},{"Add":"(e : Equivalence a) => Uninhabited (LinkedListEquiv @{e} Nil (h :: t)) where"},{"Add":" uninhabited BothEmpty impossible"},{"Add":" uninhabited (EquivHeadAndTail h t) impossible"},{"Add":""},{"Add":"public export"},{"Add":"(e : Equivalence a) => Uninhabited (LinkedListEquiv @{e} (h :: t) Nil) where"},{"Add":" uninhabited BothEmpty impossible"},{"Add":" uninhabited (EquivHeadAndTail h t) impossible"},{"Add":""},{"Add":"public export"},{"Add":"fromNotEquivHead : (e : Equivalence t) => {a, b : t} -> (ok: Not (Equiv a b))"},{"Add":" -> Not (LinkedListEquiv @{e} (a :: x) (b :: y))"},{"Add":"fromNotEquivHead ctr (EquivHeadAndTail prf _) = ctr prf"},{"Add":""},{"Add":"public export"},{"Add":"fromNotEquivTail : (e : Equivalence t) => (ok: Not (LinkedListEquiv @{e} x y))"},{"Add":" -> Not (LinkedListEquiv @{e} (a :: x) (b :: y))"},{"Add":"fromNotEquivTail ctr (EquivHeadAndTail _ prf) = ctr prf"},{"Add":""},{"Add":"decLinkedListEquiv : (e : Equivalence t) => (a, b : LinkedList t)"},{"Add":" -> Dec (LinkedListEquiv @{e} a b)"},{"Add":"decLinkedListEquiv Nil Nil = Yes BothEmpty"},{"Add":"decLinkedListEquiv Nil (_::_) = No absurd"},{"Add":"decLinkedListEquiv (_::_) Nil = No absurd"},{"Add":"decLinkedListEquiv @{e} (h1::t1) (h2::t2) ="},{"Add":" case (decEquiv @{e} h1 h2, decLinkedListEquiv t1 t2) of"},{"Add":" (Yes prf1, Yes prf2) => Yes $ EquivHeadAndTail prf1 prf2"},{"Add":" (Yes prf1, No ctra2) => No $ fromNotEquivTail @{e} ctra2"},{"Add":" (No ctra1, _) => No $ fromNotEquivHead @{e} ctra1"},{"Add":""},{"Add":"public export"},{"Add":"(Equivalence t) => Equivalence (LinkedList t) where"},{"Add":" Equiv = LinkedListEquiv"},{"Add":" decEquiv = decLinkedListEquiv"}]}},{"FileAdd":{"meta":{"basename":"Basic.idr","metadata":0},"context":[{"change":0,"pos":413}],"contents":[{"Add":"module Data.LinkedList.Basic"},{"Add":""},{"Add":"import Builtin"},{"Add":""},{"Add":"%default total"},{"Add":""},{"Add":"infixr 7 ::"},{"Add":""},{"Add":"public export"},{"Add":"data LinkedList t = Nil | (::) t (LinkedList t)"},{"Add":""},{"Add":"public export"},{"Add":"concat : LinkedList t -> LinkedList t -> LinkedList t"},{"Add":"concat Nil y = y"},{"Add":"concat (x::xs) y = x :: concat xs y"},{"Add":""},{"Add":"export"},{"Add":"proofConcatRightIdentity : (l : LinkedList t) -> concat l Nil = l"},{"Add":"proofConcatRightIdentity Nil = Refl"},{"Add":"proofConcatRightIdentity (x::xs) = rewrite proofConcatRightIdentity xs in Refl"}]}},{"FileAdd":{"meta":{"basename":"Applicative.idr","metadata":0},"context":[{"change":0,"pos":413}],"contents":[{"Add":"module Data.LinkedList.Applicative"},{"Add":""},{"Add":"import Builtin"},{"Add":""},{"Add":"import Algebra.Control.Functor"},{"Add":"import Algebra.Control.Applicative"},{"Add":""},{"Add":"import public Data.LinkedList.Basic"},{"Add":"import public Data.LinkedList.Functor"},{"Add":""},{"Add":"%default total"},{"Add":""},{"Add":"public export"},{"Add":"app : LinkedList (a -> b) -> LinkedList a -> LinkedList b"},{"Add":"app Nil _ = Nil"},{"Add":"app (f::fs) l = (f <$> l) `concat` app fs l"},{"Add":""},{"Add":"public export"},{"Add":"appNil : (f : LinkedList (a -> b)) -> f `app` Nil = Nil"},{"Add":"appNil Nil = Refl"},{"Add":"appNil (f::fs) = rewrite appNil fs in Refl"},{"Add":""},{"Add":"public export"},{"Add":"Applicative LinkedList where"},{"Add":" pure x = [x]"},{"Add":""},{"Add":" (<*>) = app"},{"Add":""},{"Add":" proofIdentity Nil = Refl"},{"Add":" proofIdentity (_::xs) with (Functor.proofIdentity xs)"},{"Add":" proofIdentity (_::xs) | prf ="},{"Add":" rewrite proofConcatRightIdentity (identity <$> xs) in"},{"Add":" rewrite prf in Refl"},{"Add":""},{"Add":" proofHomomorphism f x = Refl"},{"Add":""},{"Add":" proofInterchange Nil x = Refl"},{"Add":" proofInterchange (f::fs) x = rewrite proofInterchange fs x in Refl"},{"Add":""},{"Add":" proofComposition Nil Nil _ = Refl"},{"Add":" proofComposition Nil (_::gs) _ ="},{"Add":" rewrite appNil gs in"},{"Add":" -- rewrite proofConcatRightIdentity ((.) <$> gs) in"},{"Add":" ?holeComposition1"},{"Add":" proofComposition (f::fs) gs _ ="},{"Add":" -- rewrite proofConcatRightIdentity ((.) <$> gs) in"},{"Add":" ?holeComposition2"}]}}],"owner":"fabian","repo":"veribase-idr2","token":"hqWt1NxuPtHMi5D5ItGG8L+tMzpBpC1u2DWZwvOgxs4=","login":null}

…

Dependencies

Change contents