{"header":{"message":"Refactor","description":null,"timestamp":"2021-06-12T01:47:18.615191967Z","authors":[{"email":"fabianhjr@protonmail.com","full_name":"Fabián Heredia Montiel","name":"fabian"}]},"hash":"RUIGRXTKM6BQ532W7KU3RKDXMRNRGDVGMA2ODMX2D2F3PCLF3GAQC","authors":[],"deps":{"hashes":[["RUIGRXTKM6BQ532W7KU3RKDXMRNRGDVGMA2ODMX2D2F3PCLF3GAQC","Refactor"],["AA",null],["XNMLOZPY2VS5RTP4CO2MN3LSOHL7UGGWO7MPI5ARMYFS5EJMLGOAC","Reorder proofs in Applicative"],["WJJ6PMS6GYR5NIQI6Q6YH6WQSTJ3U56F3KZJOSYHTRAZ5MKIPXAAC","Refactor"],["TN3PKVP3EMBILQKHDKEJMCJU5U6E3BLDQMMIUV2WE3XQ4HTCPBRAC","Add `GTE` and `GT` to Preorder and Order"],["BLJHEFB7SWAE4XB3GUAWA6TOVFKONOZO7URKJVSUNXGRXLKZHXOQC","A lot of Natural Proofs"],["6D4TYQRJMN6QEKASHJ3ZN3E7TXF5IEQ3G4ATTZZ5AZC56VXMWFZAC","Add `Algebra.Equivalence`"],["K6VKF3FC5BN3ODMH5GNGUTYN6NSNIUXYYOBMYKG2BMGXJOEKOH5AC","Implement Natural Preorder"],["NYMIFK2WBHU4G34QF4GZP63ATL2EQC6PLAQLWZMUTPDGDPQUEKVQC","Make a HelloWorld sample work"],["VE7QTPXHFI2SKUADFYESQPELRZZF2JQRPLTFI4TL6J2PALARUO7QC","Add `Algebra.Applicative`"],["7SFN5S4CUZZL523G6RHETVEJCJUIMXH2YPDTRKQWCGZTDYNWW4LQC","Add `Algebra.Functor`"],["GEBWJGHFGLPFE6PGT5D7W3PL57NPMQRPDUK54GTN4344W6QT7DPAC","Implement Boolean Monoids"],["CO3C7GSZ2X62ALXW2EAWDHCRSXCNVKIIHCL47GYZ32OHZER4NLZQC","Create Data.Either"],["Y25HAVMY4WAD43DQ5PHLHUPDKW7X6DWJVP3VKYVQ3AE25S6ESSXAC","Implement Boolean Semilattices"],["K7TT3LDM6HYYXLSYFSJZRQZ6GOGTDJ7F5KFU7GBPJOKN2DHJLHMQC","Add `Data.LinkedList`"],["YEPLQQC3GXCKIMKHMG4QF42ZVEBE3AV2P7MXD2FBA4XAJSQNIBEQC","Implement PrimIO, Control.IO, Control.Console"],["ZADJ47JPO7SQJNR5OMSJSYPUGDVBVHGBXZBEKTA7FEK7F5437MSAC","Implement `Order Natural`"],["YE3EAD3XYKXRHEJN4VLBVBQM2EISKFHAESPOZ6S4QMLA6YZEVDQQC","Fix `Equiv` signatures to take into account multiple implementations of interface"],["TTGQ6KKFCCLVNZDOWWBOOXKEKMCELYB5ULXLXWY4THZMZCUASGWQC","Implement `minus` and part of `mult`"],["AYH2HO67CJQTXMZO5JEFBXSDAVUH4NVX42VAQMPJIQUGX7UFW3IAC","Add missing `%default total` declarations"],["ZQLW6BX54QFHXQHJTOQ7KW3TBNE6VZZGTD3FPUOLVULYRS66NGLQC","Refactor to simplify Optional's decEquiv"],["XNPLRKJ4ZK442XNJ5BC7TO3DKXGXFSOSGBZBPW5HZZDHY3IVD6FAC","Init"],["ZJMXCVWEW2XHBZGNQUHTW7JRIAEAE5UDTASSD75WJG55MDOUZ3MAC","Implement `LinkedList`'s `Monoid` interface"],["46ULZLRWCBDYLPE7Z4UU4G6ELIHVUWF7WUJIKBCMS3QVHTGA2L4QC","Add Semilattices"],["4KXMGXQ6PTWVMINMKRCQE7DIJXUYMO7SVNR6AQ243QULY7IZLUYAC","Refactor Algebra"],["XJZ5YZW6TIBBMPL2TGEA2ERD2UYZ4PIXNSV25ETLUVPLDM3RA5EQC","Add Natural"],["LHFSZWK3U3RF4SBC2OY44PQ47GDELJ4NZOVRR2OBK3YVNNYKSDLAC","Add Preorder and Order"],["2DQ47UENKWPVS6XYO73Q2KCHTNG6GQVP2CKP24V2OQ4F4T3KAFMAC","Implemente Data.Boolean Order"],["LDJ4DDJZJV3W2UZIK6USOW5IADAWHDYM3EMZNCBFDKCXFYVS3WCAC","Implement `Natural.plus`"],["4WZ2PYVOKVZFB6Q44LR6APOSMZTUR566HI5IOFLDCA5C7RQRMFRAC","Add `Data.LinkedList` `Monad` Instance"],["PUFI27GBQLTD64UCR35JZOWINUF2A5BWFUI5G6ZQN3UFQZPZB54AC","Implement `Data.LinkedList` `Applicative` (Mostly)"],["DNU6TYDJ7M3S62NXVOSK5TR4Q77SQRAS4T2VFLZALFIR2JARYS7QC","Implement `Applicative` for `Data.Optional`"]],"deps":["XNMLOZPY2VS5RTP4CO2MN3LSOHL7UGGWO7MPI5ARMYFS5EJMLGOAC","WJJ6PMS6GYR5NIQI6Q6YH6WQSTJ3U56F3KZJOSYHTRAZ5MKIPXAAC","TN3PKVP3EMBILQKHDKEJMCJU5U6E3BLDQMMIUV2WE3XQ4HTCPBRAC","BLJHEFB7SWAE4XB3GUAWA6TOVFKONOZO7URKJVSUNXGRXLKZHXOQC"],"known":["XNPLRKJ4ZK442XNJ5BC7TO3DKXGXFSOSGBZBPW5HZZDHY3IVD6FAC","6D4TYQRJMN6QEKASHJ3ZN3E7TXF5IEQ3G4ATTZZ5AZC56VXMWFZAC","7SFN5S4CUZZL523G6RHETVEJCJUIMXH2YPDTRKQWCGZTDYNWW4LQC","ZQLW6BX54QFHXQHJTOQ7KW3TBNE6VZZGTD3FPUOLVULYRS66NGLQC","K7TT3LDM6HYYXLSYFSJZRQZ6GOGTDJ7F5KFU7GBPJOKN2DHJLHMQC","VE7QTPXHFI2SKUADFYESQPELRZZF2JQRPLTFI4TL6J2PALARUO7QC","YE3EAD3XYKXRHEJN4VLBVBQM2EISKFHAESPOZ6S4QMLA6YZEVDQQC","DNU6TYDJ7M3S62NXVOSK5TR4Q77SQRAS4T2VFLZALFIR2JARYS7QC","ZJMXCVWEW2XHBZGNQUHTW7JRIAEAE5UDTASSD75WJG55MDOUZ3MAC","PUFI27GBQLTD64UCR35JZOWINUF2A5BWFUI5G6ZQN3UFQZPZB54AC","4WZ2PYVOKVZFB6Q44LR6APOSMZTUR566HI5IOFLDCA5C7RQRMFRAC","GEBWJGHFGLPFE6PGT5D7W3PL57NPMQRPDUK54GTN4344W6QT7DPAC","CO3C7GSZ2X62ALXW2EAWDHCRSXCNVKIIHCL47GYZ32OHZER4NLZQC","4KXMGXQ6PTWVMINMKRCQE7DIJXUYMO7SVNR6AQ243QULY7IZLUYAC","LHFSZWK3U3RF4SBC2OY44PQ47GDELJ4NZOVRR2OBK3YVNNYKSDLAC","2DQ47UENKWPVS6XYO73Q2KCHTNG6GQVP2CKP24V2OQ4F4T3KAFMAC","46ULZLRWCBDYLPE7Z4UU4G6ELIHVUWF7WUJIKBCMS3QVHTGA2L4QC","Y25HAVMY4WAD43DQ5PHLHUPDKW7X6DWJVP3VKYVQ3AE25S6ESSXAC","AYH2HO67CJQTXMZO5JEFBXSDAVUH4NVX42VAQMPJIQUGX7UFW3IAC","YEPLQQC3GXCKIMKHMG4QF42ZVEBE3AV2P7MXD2FBA4XAJSQNIBEQC","NYMIFK2WBHU4G34QF4GZP63ATL2EQC6PLAQLWZMUTPDGDPQUEKVQC","XJZ5YZW6TIBBMPL2TGEA2ERD2UYZ4PIXNSV25ETLUVPLDM3RA5EQC","K6VKF3FC5BN3ODMH5GNGUTYN6NSNIUXYYOBMYKG2BMGXJOEKOH5AC","ZADJ47JPO7SQJNR5OMSJSYPUGDVBVHGBXZBEKTA7FEK7F5437MSAC","LDJ4DDJZJV3W2UZIK6USOW5IADAWHDYM3EMZNCBFDKCXFYVS3WCAC","TTGQ6KKFCCLVNZDOWWBOOXKEKMCELYB5ULXLXWY4THZMZCUASGWQC"]},"hunks":[{"Replacement":{"inode":{"change":6,"pos":30},"path":"src/Data/Optional.idr","line":48,"ins":{"up_context":[{"change":6,"pos":380}],"down_context":[{"change":6,"pos":439}],"flag":"BLOCK","start":0,"end":57,"inode":{"change":6,"pos":30}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":380},"to":{"change":6,"start":380,"end":439},"introduced_by":6}],"inode":{"change":6,"pos":30}},"ins_contents":[{"Add":" f <$> Nothing = Nothing"},{"Add":" f <$> (Some a) = Some $ f a"}],"del_contents":[{"Del":" map f Nothing = Nothing\n map f (Some a) = Some . f $ a\n"}]}},{"Replacement":{"inode":{"change":6,"pos":31},"path":"src/Data/Natural.idr","line":53,"ins":{"up_context":[{"change":6,"pos":1192}],"down_context":[{"change":6,"pos":64}],"flag":"BLOCK","start":58,"end":116,"inode":{"change":6,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":1192},"to":{"change":6,"start":1192,"end":1249},"introduced_by":6}],"inode":{"change":6,"pos":31}},"ins_contents":[{"Add":" No cp => No $ proofNotEquivThenNotSuccesorEquiv cp"}],"del_contents":[{"Del":" No cp => No $ proofNotEquivThenNotSuccesorEquiv cp\n"}]}},{"Replacement":{"inode":{"change":6,"pos":31},"path":"src/Data/Natural.idr","line":60,"ins":{"up_context":[{"change":6,"pos":130}],"down_context":[{"change":6,"pos":234}],"flag":"BLOCK","start":117,"end":225,"inode":{"change":6,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":130},"to":{"change":6,"start":130,"end":234},"introduced_by":6}],"inode":{"change":6,"pos":31}},"ins_contents":[{"Add":" ZeroLTEAny : NaturalLTE Zero y"},{"Add":" SuccesorLTE : NaturalLTE x y -> NaturalLTE (Succesor x) (Succesor y)"}],"del_contents":[{"Del":" ZeroLTEAny : NaturalLTE Zero y\n SuccesorLTE : NaturalLTE x y -> NaturalLTE (Succesor x) (Succesor y)\n"}]}},{"Replacement":{"inode":{"change":6,"pos":31},"path":"src/Data/Natural.idr","line":70,"ins":{"up_context":[{"change":6,"pos":116}],"down_context":[{"change":6,"pos":173}],"flag":"BLOCK","start":226,"end":279,"inode":{"change":6,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":116},"to":{"change":6,"start":116,"end":173},"introduced_by":6}],"inode":{"change":6,"pos":31}},"ins_contents":[{"Add":"proofLTEThenLTESuccesor ZeroLTEAny = ZeroLTEAny"}],"del_contents":[{"Del":"proofLTEThenLTESuccesor {x=Zero} ZeroLTEAny = ZeroLTEAny\n"}]}},{"Replacement":{"inode":{"change":6,"pos":31},"path":"src/Data/Natural.idr","line":86,"ins":{"up_context":[{"change":6,"pos":774}],"down_context":[{"change":6,"pos":827}],"flag":"BLOCK","start":280,"end":334,"inode":{"change":6,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":774},"to":{"change":6,"start":774,"end":827},"introduced_by":6}],"inode":{"change":6,"pos":31}},"ins_contents":[{"Add":" No cp => No $ proofNotLTEThenNotSuccesorLTE cp"}],"del_contents":[{"Del":" No cp => No $ proofNotLTEThenNotSuccesorLTE cp\n"}]}},{"Replacement":{"inode":{"change":6,"pos":31},"path":"src/Data/Natural.idr","line":106,"ins":{"up_context":[{"change":6,"pos":545}],"down_context":[{"change":6,"pos":599}],"flag":"BLOCK","start":335,"end":390,"inode":{"change":6,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":545},"to":{"change":6,"start":545,"end":599},"introduced_by":6}],"inode":{"change":6,"pos":31}},"ins_contents":[{"Add":" No cp => No $ proofNotLTEThenNotSuccesorLTE cp"}],"del_contents":[{"Del":" No cp => No $ proofNotLTEThenNotSuccesorLTE cp\n"}]}},{"Replacement":{"inode":{"change":6,"pos":31},"path":"src/Data/Natural.idr","line":118,"ins":{"up_context":[{"change":6,"pos":1108}],"down_context":[{"change":6,"pos":1145}],"flag":"BLOCK","start":391,"end":432,"inode":{"change":6,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":1108},"to":{"change":6,"start":1108,"end":1145},"introduced_by":6}],"inode":{"change":6,"pos":31}},"ins_contents":[{"Add":" Left l => Left $ SuccesorLTE l"}],"del_contents":[{"Del":" Left l => Left $ SuccesorLTE l\n"}]}},{"Edit":{"inode":{"change":6,"pos":31},"path":"src/Data/Natural.idr","line":141,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":86},"to":{"change":5,"start":86,"end":94},"introduced_by":5}],"inode":{"change":6,"pos":31}}},"contents":[{"Del":"partial\n"}]}},{"Replacement":{"inode":{"change":6,"pos":31},"path":"src/Data/Natural.idr","line":245,"ins":{"up_context":[{"change":6,"pos":1330}],"down_context":[{"change":6,"pos":1338}],"flag":"BLOCK","start":433,"end":447,"inode":{"change":6,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":1330},"to":{"change":6,"start":1330,"end":1338},"introduced_by":6}],"inode":{"change":6,"pos":31}},"ins_contents":[{"Add":"public export"}],"del_contents":[{"Del":"partial\n"}]}},{"Edit":{"inode":{"change":6,"pos":17},"path":"src/Data/LinkedList.idr","line":7,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":58},"to":{"change":6,"start":752,"end":787},"introduced_by":6}],"inode":{"change":6,"pos":17}}},"contents":[{"Del":"import Algebra.Control.Applicative\n"}]}},{"Edit":{"inode":{"change":6,"pos":17},"path":"src/Data/LinkedList.idr","line":8,"atom":{"NewVertex":{"up_context":[{"change":6,"pos":854}],"down_context":[{"change":6,"pos":854}],"flag":"BLOCK","start":448,"end":483,"inode":{"change":6,"pos":17}}},"contents":[{"Add":"import Algebra.Control.Applicative"}]}},{"Edit":{"inode":{"change":6,"pos":17},"path":"src/Data/LinkedList.idr","line":12,"atom":{"NewVertex":{"up_context":[{"change":6,"pos":511}],"down_context":[{"change":6,"pos":883}],"flag":"BLOCK","start":484,"end":515,"inode":{"change":6,"pos":17}}},"contents":[{"Add":"import Algebra.Group.Semigroup"}]}},{"Edit":{"inode":{"change":6,"pos":17},"path":"src/Data/LinkedList.idr","line":14,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":911},"to":{"change":6,"start":512,"end":543},"introduced_by":6}],"inode":{"change":6,"pos":17}}},"contents":[{"Del":"import Algebra.Group.Semigroup\n"}]}},{"Edit":{"inode":{"change":6,"pos":17},"path":"src/Data/LinkedList.idr","line":41,"atom":{"EdgeMap":{"edges":[{"previous":"","flag":"DELETED","from":{"change":6,"pos":584},"to":{"change":6,"start":921,"end":963},"introduced_by":6},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":921},"to":{"change":6,"start":921,"end":963},"introduced_by":6}],"inode":{"change":6,"pos":17}}},"contents":[{"Del":"fromNotEquivHead ctr BothEmpty impossible\n"}]}},{"Edit":{"inode":{"change":6,"pos":17},"path":"src/Data/LinkedList.idr","line":46,"atom":{"EdgeMap":{"edges":[{"previous":"","flag":"DELETED","from":{"change":6,"pos":786},"to":{"change":6,"start":1126,"end":1168},"introduced_by":6},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":1126},"to":{"change":6,"start":1126,"end":1168},"introduced_by":6}],"inode":{"change":6,"pos":17}}},"contents":[{"Del":"fromNotEquivTail ctr BothEmpty impossible\n"}]}},{"Replacement":{"inode":{"change":6,"pos":17},"path":"src/Data/LinkedList.idr","line":49,"ins":{"up_context":[{"change":6,"pos":887}],"down_context":[{"change":6,"pos":1087}],"flag":"BLOCK","start":516,"end":687,"inode":{"change":6,"pos":17}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":887},"to":{"change":6,"start":887,"end":1087},"introduced_by":6}],"inode":{"change":6,"pos":17}},"ins_contents":[{"Add":"decLinkedListEquiv Nil Nil = Yes BothEmpty"},{"Add":"decLinkedListEquiv Nil (_::_) = No absurd"},{"Add":"decLinkedListEquiv (_::_) Nil = No absurd"},{"Add":"decLinkedListEquiv @{e} (h1::t1) (h2::t2) ="}],"del_contents":[{"Del":"decLinkedListEquiv Nil Nil = Yes $ BothEmpty\ndecLinkedListEquiv Nil (_ :: _) = No $ absurd\ndecLinkedListEquiv (_ :: _) Nil = No $ absurd\ndecLinkedListEquiv @{e} (h1 :: t1) (h2 :: t2) = assert_total $\n"}]}},{"Replacement":{"inode":{"change":6,"pos":17},"path":"src/Data/LinkedList.idr","line":94,"ins":{"up_context":[{"change":6,"pos":1758}],"down_context":[{"change":6,"pos":1808}],"flag":"BLOCK","start":688,"end":738,"inode":{"change":6,"pos":17}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":1758},"to":{"change":6,"start":1758,"end":1808},"introduced_by":6}],"inode":{"change":6,"pos":17}},"ins_contents":[{"Add":" _ <$> Nil = Nil"},{"Add":" f <$> (h::t) = f h :: f <$> t"}],"del_contents":[{"Del":" map _ Nil = Nil\n map f (h::t) = f h :: map f t\n"}]}},{"Replacement":{"inode":{"change":6,"pos":17},"path":"src/Data/LinkedList.idr","line":98,"ins":{"up_context":[{"change":6,"pos":1836}],"down_context":[{"change":6,"pos":1935}],"flag":"BLOCK","start":739,"end":838,"inode":{"change":6,"pos":17}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":1836},"to":{"change":6,"start":1836,"end":1935},"introduced_by":6}],"inode":{"change":6,"pos":17}},"ins_contents":[{"Add":" proofIdentity (_::t) with (proofIdentity t)"},{"Add":" proofIdentity (_::_) | prf = rewrite prf in Refl"}],"del_contents":[{"Del":" proofIdentity (h::t) with (proofIdentity t)\n proofIdentity (h::t) | prf = rewrite prf in Refl\n"}]}},{"Replacement":{"inode":{"change":6,"pos":17},"path":"src/Data/LinkedList.idr","line":101,"ins":{"up_context":[{"change":6,"pos":1936}],"down_context":[{"change":6,"pos":28}],"flag":"BLOCK","start":839,"end":947,"inode":{"change":6,"pos":17}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":1936},"to":{"change":6,"start":1936,"end":2041},"introduced_by":6}],"inode":{"change":6,"pos":17}},"ins_contents":[{"Add":" proofComposition f g Nil = Refl"},{"Add":" proofComposition f g (_::t) = rewrite proofComposition f g t in Refl"}],"del_contents":[{"Del":" proofComposition f g Nil = Refl\n proofComposition f g (h::t) = rewrite proofComposition f g t in Refl\n"}]}},{"Replacement":{"inode":{"change":6,"pos":17},"path":"src/Data/LinkedList.idr","line":107,"ins":{"up_context":[{"change":6,"pos":121}],"down_context":[{"change":6,"pos":157}],"flag":"BLOCK","start":948,"end":986,"inode":{"change":6,"pos":17}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":121},"to":{"change":6,"start":121,"end":157},"introduced_by":6}],"inode":{"change":6,"pos":17}},"ins_contents":[{"Add":"app (f::fs) l = (f <$> l) <> app fs l"}],"del_contents":[{"Del":"app (f::fs) l = map f l <> app fs l\n"}]}},{"Replacement":{"inode":{"change":6,"pos":17},"path":"src/Data/LinkedList.idr","line":123,"ins":{"up_context":[{"change":6,"pos":493}],"down_context":[{"change":6,"pos":538}],"flag":"BLOCK","start":987,"end":1032,"inode":{"change":6,"pos":17}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":493},"to":{"change":6,"start":493,"end":538},"introduced_by":6}],"inode":{"change":6,"pos":17}},"ins_contents":[{"Add":" rewrite concatNil (identity <$> xs) in"}],"del_contents":[{"Del":" rewrite concatNil (map identity xs) in\n"}]}},{"Replacement":{"inode":{"change":6,"pos":17},"path":"src/Data/LinkedList.idr","line":134,"ins":{"up_context":[{"change":6,"pos":795}],"down_context":[{"change":6,"pos":836}],"flag":"BLOCK","start":1033,"end":1074,"inode":{"change":6,"pos":17}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":795},"to":{"change":6,"start":795,"end":836},"introduced_by":6}],"inode":{"change":6,"pos":17}},"ins_contents":[{"Add":" -- rewrite concatNil ((.) <$> gs) in"}],"del_contents":[{"Del":" -- rewrite concatNil (map (.) gs) in\n"}]}},{"Edit":{"inode":{"change":6,"pos":17},"path":"src/Data/LinkedList.idr","line":137,"atom":{"NewVertex":{"up_context":[{"change":6,"pos":892}],"down_context":[{"change":6,"pos":892}],"flag":"BLOCK","start":1075,"end":1116,"inode":{"change":6,"pos":17}}},"contents":[{"Add":" -- rewrite concatNil ((.) <$> gs) in"}]}},{"Replacement":{"inode":{"change":6,"pos":13},"path":"src/Data/Either.idr","line":16,"ins":{"up_context":[{"change":6,"pos":218}],"down_context":[{"change":6,"pos":277}],"flag":"BLOCK","start":1117,"end":1176,"inode":{"change":6,"pos":13}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":218},"to":{"change":6,"start":218,"end":277},"introduced_by":6}],"inode":{"change":6,"pos":13}},"ins_contents":[{"Add":" f <$> (Left x) = Left x"},{"Add":" f <$> (Right x) = Right $ f x"}],"del_contents":[{"Del":" map f (Left x) = Left x\n map f (Right x) = Right $ f x\n"}]}},{"Replacement":{"inode":{"change":6,"pos":13},"path":"src/Data/Either.idr","line":19,"ins":{"up_context":[{"change":6,"pos":278}],"down_context":[{"change":6,"pos":311}],"flag":"BLOCK","start":1177,"end":1210,"inode":{"change":6,"pos":13}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":278},"to":{"change":6,"start":278,"end":311},"introduced_by":6}],"inode":{"change":6,"pos":13}},"ins_contents":[{"Add":" proofIdentity (Left _) = Refl"}],"del_contents":[{"Del":" proofIdentity (Left _) = Refl\n"}]}},{"Replacement":{"inode":{"change":6,"pos":13},"path":"src/Data/Either.idr","line":29,"ins":{"up_context":[{"change":6,"pos":484}],"down_context":[{"change":6,"pos":554}],"flag":"BLOCK","start":1211,"end":1281,"inode":{"change":6,"pos":13}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":484},"to":{"change":6,"start":484,"end":554},"introduced_by":6}],"inode":{"change":6,"pos":13}},"ins_contents":[{"Add":" (Left x) <*> _ = Left x"},{"Add":" (Right _) <*> (Left y) = Left y"}],"del_contents":[{"Del":" (Left x) <*> _ = Left x\n (Right _) <*> (Left y) = Left y\n"}]}},{"Replacement":{"inode":{"change":6,"pos":13},"path":"src/Data/Either.idr","line":41,"ins":{"up_context":[{"change":6,"pos":771}],"down_context":[{"change":6,"pos":915}],"flag":"BLOCK","start":1282,"end":1426,"inode":{"change":6,"pos":13}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":771},"to":{"change":6,"start":771,"end":915},"introduced_by":6}],"inode":{"change":6,"pos":13}},"ins_contents":[{"Add":" proofComposition (Left _) (Left _) _ = Refl"},{"Add":" proofComposition (Left _) (Right _) _ = Refl"},{"Add":" proofComposition (Right _) (Left _) _ = Refl"}],"del_contents":[{"Del":" proofComposition (Left _) (Left _) _ = Refl\n proofComposition (Left _) (Right _) _ = Refl\n proofComposition (Right _) (Left _) _ = Refl\n"}]}},{"Replacement":{"inode":{"change":6,"pos":13},"path":"src/Data/Either.idr","line":45,"ins":{"up_context":[{"change":6,"pos":968}],"down_context":[{"change":6,"pos":987}],"flag":"BLOCK","start":1427,"end":1447,"inode":{"change":6,"pos":13}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":968},"to":{"change":6,"start":968,"end":987},"introduced_by":6}],"inode":{"change":6,"pos":13}},"ins_contents":[{"Add":" Left x => Refl"}],"del_contents":[{"Del":" Left x => Refl\n"}]}},{"Replacement":{"inode":{"change":6,"pos":13},"path":"src/Data/Either.idr","line":50,"ins":{"up_context":[{"change":6,"pos":1045}],"down_context":[{"change":6,"pos":642}],"flag":"BLOCK","start":1448,"end":1475,"inode":{"change":6,"pos":13}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":1045},"to":{"change":6,"start":615,"end":642},"introduced_by":6}],"inode":{"change":6,"pos":13}},"ins_contents":[{"Add":" (Left x) >>= _ = Left x"}],"del_contents":[{"Del":" (Left x) >>= _ = Left x\n"}]}},{"Replacement":{"inode":{"change":6,"pos":117},"path":"src/Data/Boolean.idr","line":49,"ins":{"up_context":[{"change":6,"pos":214}],"down_context":[{"change":6,"pos":212}],"flag":"BLOCK","start":1476,"end":1625,"inode":{"change":6,"pos":117}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":214},"to":{"change":6,"start":688,"end":845},"introduced_by":6}],"inode":{"change":6,"pos":117}},"ins_contents":[{"Add":" decEquiv False False = Yes BothFalse"},{"Add":" decEquiv True True = Yes BothTrue"},{"Add":" decEquiv False True = No absurd"},{"Add":" decEquiv True False = No absurd"}],"del_contents":[{"Del":" decEquiv False False = Yes $ BothFalse\n decEquiv True True = Yes $ BothTrue\n decEquiv False True = No $ absurd\n decEquiv True False = No $ absurd\n"}]}},{"Replacement":{"inode":{"change":6,"pos":117},"path":"src/Data/Boolean.idr","line":56,"ins":{"up_context":[{"change":6,"pos":297}],"down_context":[{"change":6,"pos":334}],"flag":"BLOCK","start":1626,"end":1664,"inode":{"change":6,"pos":117}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":297},"to":{"change":6,"start":297,"end":334},"introduced_by":6}],"inode":{"change":6,"pos":117}},"ins_contents":[{"Add":" TrueLTETrue : BooleanLTE True True"}],"del_contents":[{"Del":" TrueLTETrue : BooleanLTE True True\n"}]}},{"Replacement":{"inode":{"change":6,"pos":117},"path":"src/Data/Boolean.idr","line":68,"ins":{"up_context":[{"change":6,"pos":562}],"down_context":[{"change":6,"pos":595}],"flag":"BLOCK","start":1665,"end":1699,"inode":{"change":6,"pos":117}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":562},"to":{"change":6,"start":562,"end":595},"introduced_by":6}],"inode":{"change":6,"pos":117}},"ins_contents":[{"Add":" decLTE True False = No absurd"}],"del_contents":[{"Del":" decLTE True False = No absurd\n"}]}},{"Replacement":{"inode":{"change":6,"pos":117},"path":"src/Data/Boolean.idr","line":93,"ins":{"up_context":[{"change":6,"pos":1264}],"down_context":[{"change":6,"pos":1296}],"flag":"BLOCK","start":1700,"end":1733,"inode":{"change":6,"pos":117}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":1264},"to":{"change":6,"start":1264,"end":1296},"introduced_by":6}],"inode":{"change":6,"pos":117}},"ins_contents":[{"Add":" decLT False False = No absurd"}],"del_contents":[{"Del":" decLT False False = No absurd\n"}]}},{"Replacement":{"inode":{"change":6,"pos":117},"path":"src/Data/Boolean.idr","line":95,"ins":{"up_context":[{"change":6,"pos":1334}],"down_context":[{"change":6,"pos":1366}],"flag":"BLOCK","start":1734,"end":1767,"inode":{"change":6,"pos":117}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":1334},"to":{"change":6,"start":1334,"end":1366},"introduced_by":6}],"inode":{"change":6,"pos":117}},"ins_contents":[{"Add":" decLT True _ = No absurd"}],"del_contents":[{"Del":" decLT True _ = No absurd\n"}]}},{"Replacement":{"inode":{"change":6,"pos":117},"path":"src/Data/Boolean.idr","line":159,"ins":{"up_context":[{"change":3,"pos":182}],"down_context":[{"change":6,"pos":956}],"flag":"BLOCK","start":1768,"end":1813,"inode":{"change":6,"pos":117}},"del":{"edges":[{"previous":"","flag":"DELETED","from":{"change":3,"pos":182},"to":{"change":6,"start":912,"end":956},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":912},"to":{"change":6,"start":912,"end":956},"introduced_by":6}],"inode":{"change":6,"pos":117}},"ins_contents":[{"Add":" proofLeftIdentity = proofDisjLeftIdentity"}],"del_contents":[{"Del":" proofLeftIdentity = proofDisjLeftIdentity\n"}]}},{"Replacement":{"inode":{"change":6,"pos":117},"path":"src/Data/Boolean.idr","line":202,"ins":{"up_context":[{"change":6,"pos":1520}],"down_context":[{"change":6,"pos":1552}],"flag":"BLOCK","start":1814,"end":1847,"inode":{"change":6,"pos":117}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":1520},"to":{"change":6,"start":1520,"end":1552},"introduced_by":6}],"inode":{"change":6,"pos":117}},"ins_contents":[{"Add":" proofAssociativity True b c ="}],"del_contents":[{"Del":" proofAssociativity True b c =\n"}]}},{"Replacement":{"inode":{"change":6,"pos":117},"path":"src/Data/Boolean.idr","line":241,"ins":{"up_context":[{"change":6,"pos":721}],"down_context":[{"change":6,"pos":1049}],"flag":"BLOCK","start":1848,"end":1930,"inode":{"change":6,"pos":117}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":721},"to":{"change":6,"start":721,"end":1049},"introduced_by":6}],"inode":{"change":6,"pos":117}},"ins_contents":[{"Add":" proofGreatestLowerBound False y z FalseLTEAny FalseLTEAny = FalseLTEAny"}],"del_contents":[{"Del":" proofGreatestLowerBound False False False FalseLTEAny FalseLTEAny = FalseLTEAny\n proofGreatestLowerBound False False True FalseLTEAny FalseLTEAny = FalseLTEAny\n proofGreatestLowerBound False True False FalseLTEAny FalseLTEAny = FalseLTEAny\n proofGreatestLowerBound False True True FalseLTEAny FalseLTEAny = FalseLTEAny\n"}]}},{"Replacement":{"inode":{"change":6,"pos":2100},"path":"src/Control/IO.idr","line":16,"ins":{"up_context":[{"change":6,"pos":2379}],"down_context":[{"change":6,"pos":2443}],"flag":"BLOCK","start":1931,"end":1995,"inode":{"change":6,"pos":2100}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":2379},"to":{"change":6,"start":2379,"end":2443},"introduced_by":6}],"inode":{"change":6,"pos":2100}},"ins_contents":[{"Add":" f <$> (MkIO p) = MkIO (p `prim__io_bind` (prim__io_pure . f))"}],"del_contents":[{"Del":" map f (MkIO p) = MkIO (p `prim__io_bind` (prim__io_pure . f))\n"}]}},{"Replacement":{"inode":{"change":6,"pos":12},"path":"src/Algebra/Relation/Order.idr","line":19,"ins":{"up_context":[{"change":6,"pos":430}],"down_context":[{"change":4,"pos":66}],"flag":"BLOCK","start":1996,"end":2105,"inode":{"change":6,"pos":12}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":430},"to":{"change":6,"start":27,"end":112},"introduced_by":6}],"inode":{"change":6,"pos":12}},"ins_contents":[{"Add":" proofLTEThenLTOrEquiv : (x, y : t) -> x `LTE` y"},{"Add":" -> Either (x `LT` y) (x `Equiv` y)"}],"del_contents":[{"Del":" proofLTEThenLTOrEquiv : (x, y : t) -> x `LTE` y -> Either (x `LT` y) (x `Equiv` y)\n"}]}},{"Replacement":{"inode":{"change":6,"pos":581},"path":"src/Algebra/Lattice/MeetSemilattice.idr","line":21,"ins":{"up_context":[{"change":6,"pos":1022}],"down_context":[],"flag":"BLOCK","start":2106,"end":2218,"inode":{"change":6,"pos":581}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":1022},"to":{"change":6,"start":1022,"end":1108},"introduced_by":6}],"inode":{"change":6,"pos":581}},"ins_contents":[{"Add":" proofGreatestLowerBound : (b, x, y : t) -> b `LTE` x -> b `LTE` y"},{"Add":" -> b `LTE` x /\\ y"}],"del_contents":[{"Del":" proofGreatestLowerBound : (b, x, y : t) -> b `LTE` x -> b `LTE` y -> b `LTE` x /\\ y\n"}]}},{"Replacement":{"inode":{"change":6,"pos":33},"path":"src/Algebra/Lattice/JoinSemilattice.idr","line":21,"ins":{"up_context":[{"change":6,"pos":474}],"down_context":[],"flag":"BLOCK","start":2219,"end":2326,"inode":{"change":6,"pos":33}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":474},"to":{"change":6,"start":474,"end":558},"introduced_by":6}],"inode":{"change":6,"pos":33}},"ins_contents":[{"Add":" proofLeastUpperBound : (b, x, y : t) -> x `LTE` b -> y `LTE` b"},{"Add":" -> x \\/ y `LTE` b"}],"del_contents":[{"Del":" proofLeastUpperBound : (b, x, y : t) -> x `LTE` b -> y `LTE` b -> x \\/ y `LTE` b\n"}]}},{"Edit":{"inode":{"change":6,"pos":14},"path":"src/Algebra/Control/Functor.idr","line":6,"atom":{"NewVertex":{"up_context":[{"change":6,"pos":70}],"down_context":[{"change":6,"pos":70}],"flag":"BLOCK","start":2327,"end":2341,"inode":{"change":6,"pos":14}}},"contents":[{"Add":""},{"Add":"infixl 9 <$>"}]}},{"Replacement":{"inode":{"change":6,"pos":14},"path":"src/Algebra/Control/Functor.idr","line":11,"ins":{"up_context":[{"change":6,"pos":111}],"down_context":[{"change":6,"pos":142}],"flag":"BLOCK","start":2342,"end":2375,"inode":{"change":6,"pos":14}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":111},"to":{"change":6,"start":111,"end":142},"introduced_by":6}],"inode":{"change":6,"pos":14}},"ins_contents":[{"Add":" (<$>) : (a -> b) -> t a -> t b"}],"del_contents":[{"Del":" map : (a -> b) -> t a -> t b\n"}]}},{"Replacement":{"inode":{"change":6,"pos":14},"path":"src/Algebra/Control/Functor.idr","line":13,"ins":{"up_context":[{"change":6,"pos":143}],"down_context":[],"flag":"BLOCK","start":2376,"end":2557,"inode":{"change":6,"pos":14}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":143},"to":{"change":6,"start":143,"end":301},"introduced_by":6}],"inode":{"change":6,"pos":14}},"ins_contents":[{"Add":" proofIdentity : (x : t a) -> Builtin.identity <$> x = x"},{"Add":" proofComposition : (f : a -> b) -> (g : b -> c) -> (x : t a)"},{"Add":" -> (g . f) <$> x = (g <$>) . (f <$>) $ x"}],"del_contents":[{"Del":" proofIdentity : (x : t a) -> map Builtin.identity x = x\n proofComposition : (f : a -> b) -> (g : b -> c) -> (x : t a) -> map (g . f) x = map g . map f $ x\n"}]}},{"Replacement":{"inode":{"change":6,"pos":18},"path":"src/Algebra/Control/Applicative.idr","line":18,"ins":{"up_context":[{"change":6,"pos":512}],"down_context":[{"change":2,"pos":0}],"flag":"BLOCK","start":2558,"end":2661,"inode":{"change":6,"pos":18}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":6,"pos":512},"to":{"change":6,"start":512,"end":596},"introduced_by":6}],"inode":{"change":6,"pos":18}},"ins_contents":[{"Add":" proofInterchange : (f : t (a -> b)) -> (x : a)"},{"Add":" -> f <*> pure x = pure ($ x) <*> f"}],"del_contents":[{"Del":" proofInterchange : (f : t (a -> b)) -> (x : a) -> f <*> pure x = pure ($ x) <*> f\n"}]}}],"owner":"fabian","repo":"veribase-idr2","token":"/YgRc1lpSj9gEth+/sCEKjr7Gk/OE6OaKjpOqgpXN8Y=","login":null}

…

Dependencies

Change contents