{"header":{"message":"Semigroup Natural","description":null,"timestamp":"2021-06-18T23:54:28.303408618Z","authors":[{"email":"fabianhjr@protonmail.com","full_name":"Fabián Heredia Montiel","name":"fabian"}]},"hash":"4L2YWRMCKZ56NCRC44XVDZQ5BEKHX26C4GQZ5TIL35Y33VKFTBCQC","authors":[],"deps":{"hashes":[["4L2YWRMCKZ56NCRC44XVDZQ5BEKHX26C4GQZ5TIL35Y33VKFTBCQC","Semigroup Natural"],["AA",null],["WGQEJYGCJTGLKYTOBJNBPIOBFLQMO7XDVRSK7VFNG6GKE7FGAELAC","Refactor"],["OQYT367KXCQGIZPWQXNFQB627WJGYD6T5WF4KBBXQKHN2SXL554QC","Add PrimInteger and Natural fromInteger"],["QL75BDYCNRAF2NPJP3MJHUPM6JRIGJQWK2OG2NWKBOVZUZ75CHOAC","Add Commutative Group Interfaces"],["ZJMXCVWEW2XHBZGNQUHTW7JRIAEAE5UDTASSD75WJG55MDOUZ3MAC","Implement `LinkedList`'s `Monoid` interface"],["AYH2HO67CJQTXMZO5JEFBXSDAVUH4NVX42VAQMPJIQUGX7UFW3IAC","Add missing `%default total` declarations"],["XGXJVBQB7LVLGIHMQYZRP53X7XBKDXFM4TFWDF3ZFZRPMCYPF4IAC","Implement `Natural.divRem`"],["XNPLRKJ4ZK442XNJ5BC7TO3DKXGXFSOSGBZBPW5HZZDHY3IVD6FAC","Init"],["XHAO2M2V7NLRMTG4WWRBOYMD6ACPYALUWGL7ST3PKU5LEH555C2AC","Implement `Data.Optional` `Monad` instance"],["AXIWYERYL2PU4JVN5WBIGTOLCVB2R7DVILTRJHU7WNMYPWPJNAOAC","Create `Monad` interface"],["YEPLQQC3GXCKIMKHMG4QF42ZVEBE3AV2P7MXD2FBA4XAJSQNIBEQC","Implement PrimIO, Control.IO, Control.Console"],["WJJ6PMS6GYR5NIQI6Q6YH6WQSTJ3U56F3KZJOSYHTRAZ5MKIPXAAC","Refactor"],["BLJHEFB7SWAE4XB3GUAWA6TOVFKONOZO7URKJVSUNXGRXLKZHXOQC","A lot of Natural Proofs"],["YE3EAD3XYKXRHEJN4VLBVBQM2EISKFHAESPOZ6S4QMLA6YZEVDQQC","Fix `Equiv` signatures to take into account multiple implementations of interface"],["K7TT3LDM6HYYXLSYFSJZRQZ6GOGTDJ7F5KFU7GBPJOKN2DHJLHMQC","Add `Data.LinkedList`"],["RUIGRXTKM6BQ532W7KU3RKDXMRNRGDVGMA2ODMX2D2F3PCLF3GAQC","Refactor"],["CO3C7GSZ2X62ALXW2EAWDHCRSXCNVKIIHCL47GYZ32OHZER4NLZQC","Create Data.Either"],["ZADJ47JPO7SQJNR5OMSJSYPUGDVBVHGBXZBEKTA7FEK7F5437MSAC","Implement `Order Natural`"],["4KXMGXQ6PTWVMINMKRCQE7DIJXUYMO7SVNR6AQ243QULY7IZLUYAC","Refactor Algebra"],["EL56EO4LYXMYS6JCOU5WVSYLAPTKIKFCHXPM4QBBFSMPTUENE5WQC","Refactor"],["LDJ4DDJZJV3W2UZIK6USOW5IADAWHDYM3EMZNCBFDKCXFYVS3WCAC","Implement `Natural.plus`"],["XJZ5YZW6TIBBMPL2TGEA2ERD2UYZ4PIXNSV25ETLUVPLDM3RA5EQC","Add Natural"],["GEBWJGHFGLPFE6PGT5D7W3PL57NPMQRPDUK54GTN4344W6QT7DPAC","Implement Boolean Monoids"],["6D4TYQRJMN6QEKASHJ3ZN3E7TXF5IEQ3G4ATTZZ5AZC56VXMWFZAC","Add `Algebra.Equivalence`"],["TTGQ6KKFCCLVNZDOWWBOOXKEKMCELYB5ULXLXWY4THZMZCUASGWQC","Implement `minus` and part of `mult`"],["NYMIFK2WBHU4G34QF4GZP63ATL2EQC6PLAQLWZMUTPDGDPQUEKVQC","Make a HelloWorld sample work"],["Y25HAVMY4WAD43DQ5PHLHUPDKW7X6DWJVP3VKYVQ3AE25S6ESSXAC","Implement Boolean Semilattices"],["LKG7V6OC5VYTHY3YWWYMIDP5O6OQCWWSMHTMJKALLNQNPOVY375AC","Implement `Algebra.Group` interfaces"],["K6VKF3FC5BN3ODMH5GNGUTYN6NSNIUXYYOBMYKG2BMGXJOEKOH5AC","Implement Natural Preorder"],["4WZ2PYVOKVZFB6Q44LR6APOSMZTUR566HI5IOFLDCA5C7RQRMFRAC","Add `Data.LinkedList` `Monad` Instance"],["LHFSZWK3U3RF4SBC2OY44PQ47GDELJ4NZOVRR2OBK3YVNNYKSDLAC","Add Preorder and Order"],["2DQ47UENKWPVS6XYO73Q2KCHTNG6GQVP2CKP24V2OQ4F4T3KAFMAC","Implemente Data.Boolean Order"]],"deps":["WGQEJYGCJTGLKYTOBJNBPIOBFLQMO7XDVRSK7VFNG6GKE7FGAELAC","OQYT367KXCQGIZPWQXNFQB627WJGYD6T5WF4KBBXQKHN2SXL554QC","QL75BDYCNRAF2NPJP3MJHUPM6JRIGJQWK2OG2NWKBOVZUZ75CHOAC"],"known":["XNPLRKJ4ZK442XNJ5BC7TO3DKXGXFSOSGBZBPW5HZZDHY3IVD6FAC","6D4TYQRJMN6QEKASHJ3ZN3E7TXF5IEQ3G4ATTZZ5AZC56VXMWFZAC","K7TT3LDM6HYYXLSYFSJZRQZ6GOGTDJ7F5KFU7GBPJOKN2DHJLHMQC","YE3EAD3XYKXRHEJN4VLBVBQM2EISKFHAESPOZ6S4QMLA6YZEVDQQC","LKG7V6OC5VYTHY3YWWYMIDP5O6OQCWWSMHTMJKALLNQNPOVY375AC","ZJMXCVWEW2XHBZGNQUHTW7JRIAEAE5UDTASSD75WJG55MDOUZ3MAC","AXIWYERYL2PU4JVN5WBIGTOLCVB2R7DVILTRJHU7WNMYPWPJNAOAC","XHAO2M2V7NLRMTG4WWRBOYMD6ACPYALUWGL7ST3PKU5LEH555C2AC","4WZ2PYVOKVZFB6Q44LR6APOSMZTUR566HI5IOFLDCA5C7RQRMFRAC","GEBWJGHFGLPFE6PGT5D7W3PL57NPMQRPDUK54GTN4344W6QT7DPAC","CO3C7GSZ2X62ALXW2EAWDHCRSXCNVKIIHCL47GYZ32OHZER4NLZQC","4KXMGXQ6PTWVMINMKRCQE7DIJXUYMO7SVNR6AQ243QULY7IZLUYAC","Y25HAVMY4WAD43DQ5PHLHUPDKW7X6DWJVP3VKYVQ3AE25S6ESSXAC","AYH2HO67CJQTXMZO5JEFBXSDAVUH4NVX42VAQMPJIQUGX7UFW3IAC","YEPLQQC3GXCKIMKHMG4QF42ZVEBE3AV2P7MXD2FBA4XAJSQNIBEQC","NYMIFK2WBHU4G34QF4GZP63ATL2EQC6PLAQLWZMUTPDGDPQUEKVQC","XJZ5YZW6TIBBMPL2TGEA2ERD2UYZ4PIXNSV25ETLUVPLDM3RA5EQC","K6VKF3FC5BN3ODMH5GNGUTYN6NSNIUXYYOBMYKG2BMGXJOEKOH5AC","EL56EO4LYXMYS6JCOU5WVSYLAPTKIKFCHXPM4QBBFSMPTUENE5WQC","ZADJ47JPO7SQJNR5OMSJSYPUGDVBVHGBXZBEKTA7FEK7F5437MSAC","LDJ4DDJZJV3W2UZIK6USOW5IADAWHDYM3EMZNCBFDKCXFYVS3WCAC","WJJ6PMS6GYR5NIQI6Q6YH6WQSTJ3U56F3KZJOSYHTRAZ5MKIPXAAC","TTGQ6KKFCCLVNZDOWWBOOXKEKMCELYB5ULXLXWY4THZMZCUASGWQC","BLJHEFB7SWAE4XB3GUAWA6TOVFKONOZO7URKJVSUNXGRXLKZHXOQC","RUIGRXTKM6BQ532W7KU3RKDXMRNRGDVGMA2ODMX2D2F3PCLF3GAQC","XGXJVBQB7LVLGIHMQYZRP53X7XBKDXFM4TFWDF3ZFZRPMCYPF4IAC"]},"hunks":[{"Edit":{"inode":{"change":5,"pos":6174},"path":"veribase.ipkg","line":24,"atom":{"NewVertex":{"up_context":[{"change":32,"pos":884}],"down_context":[{"change":5,"pos":1258}],"flag":"BLOCK","start":0,"end":26,"inode":{"change":5,"pos":6174}}},"contents":[{"Add":""},{"Add":"\t, Algebra.Ring.Semiring"}]}},{"Replacement":{"inode":{"change":5,"pos":30},"path":"src/Data/Optional.idr","line":93,"ins":{"up_context":[{"change":5,"pos":218}],"down_context":[],"flag":"BLOCK","start":27,"end":105,"inode":{"change":5,"pos":30}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":218},"to":{"change":2,"start":1053,"end":1135},"introduced_by":2}],"inode":{"change":5,"pos":30}},"ins_contents":[{"Add":" proofAssociative Nothing _ _ = Refl"},{"Add":" proofAssociative (Some _) _ _ = Refl"}],"del_contents":[{"Del":" proofAssociativity Nothing _ _ = Refl\n proofAssociativity (Some _) _ _ = Refl\n"}]}},{"Edit":{"inode":{"change":5,"pos":31},"path":"src/Data/Natural.idr","line":4,"atom":{"NewVertex":{"up_context":[{"change":5,"pos":68}],"down_context":[{"change":5,"pos":68}],"flag":"BLOCK","start":106,"end":193,"inode":{"change":5,"pos":31}}},"contents":[{"Add":""},{"Add":"import Algebra.Group.Magma"},{"Add":"import Algebra.Group.Semigroup"},{"Add":"import Algebra.Group.Monoid"}]}},{"Replacement":{"inode":{"change":5,"pos":31},"path":"src/Data/Natural.idr","line":13,"ins":{"up_context":[{"change":5,"pos":106}],"down_context":[{"change":3,"pos":823}],"flag":"BLOCK","start":194,"end":223,"inode":{"change":5,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":106},"to":{"change":5,"start":0,"end":86},"introduced_by":5}],"inode":{"change":5,"pos":31}},"ins_contents":[{"Add":"import Algebra.Ring.Semiring"}],"del_contents":[{"Del":"import Algebra.Group.Magma\nimport Algebra.Group.Semigroup\nimport Algebra.Group.Monoid\n"}]}},{"Edit":{"inode":{"change":5,"pos":31},"path":"src/Data/Natural.idr","line":209,"atom":{"NewVertex":{"up_context":[{"change":5,"pos":482}],"down_context":[{"change":5,"pos":482}],"flag":"BLOCK","start":224,"end":363,"inode":{"change":5,"pos":31}}},"contents":[{"Add":"[NaturalSumCommutativeMagma] CommutativeMagma Natural using NaturalSumMagma where"},{"Add":" proofCommutative = proofPlusCommutative"},{"Add":""},{"Add":"public export"}]}},{"Replacement":{"inode":{"change":5,"pos":31},"path":"src/Data/Natural.idr","line":214,"ins":{"up_context":[{"change":5,"pos":550}],"down_context":[{"change":5,"pos":672}],"flag":"BLOCK","start":364,"end":542,"inode":{"change":5,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":550},"to":{"change":5,"start":572,"end":616},"introduced_by":5}],"inode":{"change":5,"pos":31}},"ins_contents":[{"Add":" proofAssociative = proofPlusAssociative"},{"Add":""},{"Add":"public export"},{"Add":"[NaturalSumCommutativeSemigroup] CommutativeSemigroup Natural using NaturalSumCommutativeMagma NaturalSumSemigroup where"}],"del_contents":[{"Del":" proofAssociativity = proofPlusAssociative\n"}]}},{"Edit":{"inode":{"change":5,"pos":31},"path":"src/Data/Natural.idr","line":227,"atom":{"NewVertex":{"up_context":[{"change":5,"pos":346}],"down_context":[{"change":5,"pos":346}],"flag":"BLOCK","start":543,"end":674,"inode":{"change":5,"pos":31}}},"contents":[{"Add":"[NaturalSumCommutativeMonoid] CommutativeMonoid Natural using NaturalSumCommutativeSemigroup NaturalSumMonoid where"},{"Add":""},{"Add":"public export"}]}},{"Edit":{"inode":{"change":5,"pos":31},"path":"src/Data/Natural.idr","line":306,"atom":{"NewVertex":{"up_context":[{"change":5,"pos":2374}],"down_context":[{"change":5,"pos":2374}],"flag":"BLOCK","start":675,"end":1023,"inode":{"change":5,"pos":31}}},"contents":[{"Add":"proofMultRightDistributesPlus : (x, y, z : Natural)"},{"Add":" -> mult (plus x y) z = plus (mult x z) (mult y z)"},{"Add":"proofMultRightDistributesPlus x y z ="},{"Add":" rewrite proofMultCommutative (plus x y) z in"},{"Add":" rewrite proofMultLeftDistributesPlus z x y in"},{"Add":" rewrite proofMultCommutative z x in"},{"Add":" rewrite proofMultCommutative z y in"},{"Add":" Refl"}]}},{"Replacement":{"inode":{"change":5,"pos":31},"path":"src/Data/Natural.idr","line":321,"ins":{"up_context":[{"change":5,"pos":1408}],"down_context":[{"change":5,"pos":2376}],"flag":"BLOCK","start":1024,"end":1097,"inode":{"change":5,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":1408},"to":{"change":5,"start":1408,"end":1485},"introduced_by":5}],"inode":{"change":5,"pos":31}},"ins_contents":[{"Add":" proofAssociative x y Zero = Refl"},{"Add":" proofAssociative x y (Succesor z) ="}],"del_contents":[{"Del":" proofAssociativity x y Zero = Refl\n proofAssociativity x y (Succesor z) =\n"}]}},{"Replacement":{"inode":{"change":5,"pos":31},"path":"src/Data/Natural.idr","line":324,"ins":{"up_context":[{"change":5,"pos":2435}],"down_context":[{"change":5,"pos":2475}],"flag":"BLOCK","start":1098,"end":1136,"inode":{"change":5,"pos":31}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":2435},"to":{"change":5,"start":2435,"end":2475},"introduced_by":5}],"inode":{"change":5,"pos":31}},"ins_contents":[{"Add":" rewrite proofAssociative x y z in"}],"del_contents":[{"Del":" rewrite proofAssociativity x y z in\n"}]}},{"Edit":{"inode":{"change":5,"pos":31},"path":"src/Data/Natural.idr","line":347,"atom":{"NewVertex":{"up_context":[{"change":5,"pos":769}],"down_context":[],"flag":"BLOCK","start":1137,"end":1837,"inode":{"change":5,"pos":31}}},"contents":[{"Add":""},{"Add":"public export"},{"Add":"Semiring Natural where"},{"Add":" (+) = plus"},{"Add":" (*) = mult"},{"Add":""},{"Add":" zero = 0"},{"Add":" one = 1"},{"Add":""},{"Add":" proofSumZero = proofRightIdentity @{NaturalSumMonoid}"},{"Add":" proofSumCommutative = proofCommutative @{NaturalSumCommutativeMagma}"},{"Add":" proofSumAssociative = proofAssociative @{NaturalSumSemigroup}"},{"Add":""},{"Add":" proofMultOneLeft = proofLeftIdentity @{NaturalMultMonoid}"},{"Add":" proofMultOneRight = proofRightIdentity @{NaturalMultMonoid}"},{"Add":" proofMultAssociative = proofAssociative @{NaturalMultSemigroup}"},{"Add":""},{"Add":" proofMultDistributesSumLeft = proofMultLeftDistributesPlus"},{"Add":" proofMultDistributesSumRight = proofMultRightDistributesPlus"},{"Add":""},{"Add":" zeroAnnihilatorLeft = proofMultLeftAnnihilation"},{"Add":" zeroAnnihilatorRight = proofMultRightAnnihilation"}]}},{"Replacement":{"inode":{"change":5,"pos":17},"path":"src/Data/LinkedList.idr","line":79,"ins":{"up_context":[{"change":5,"pos":389}],"down_context":[{"change":5,"pos":1718}],"flag":"BLOCK","start":1838,"end":1949,"inode":{"change":5,"pos":17}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":389},"to":{"change":5,"start":389,"end":506},"introduced_by":5}],"inode":{"change":5,"pos":17}},"ins_contents":[{"Add":" proofAssociative Nil _ _ = Refl"},{"Add":" proofAssociative (x::xs) y z = rewrite proofAssociative xs y z in Refl"}],"del_contents":[{"Del":" proofAssociativity Nil _ _ = Refl\n proofAssociativity (x::xs) y z = rewrite proofAssociativity xs y z in Refl\n"}]}},{"Replacement":{"inode":{"change":5,"pos":17},"path":"src/Data/LinkedList.idr","line":151,"ins":{"up_context":[{"change":5,"pos":486}],"down_context":[],"flag":"BLOCK","start":1950,"end":2169,"inode":{"change":5,"pos":17}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":486},"to":{"change":5,"start":486,"end":717},"introduced_by":5}],"inode":{"change":5,"pos":17}},"ins_contents":[{"Add":" proofAssociative Nil f g = Refl"},{"Add":" proofAssociative (x::xs) f g with (f x)"},{"Add":" proofAssociative (x::xs) f g | Nil = rewrite proofAssociative xs f g in Refl"},{"Add":" proofAssociative (x::xs) f g | (r::rs) = ?holeAssociative"}],"del_contents":[{"Del":" proofAssociativity Nil f g = Refl\n proofAssociativity (x::xs) f g with (f x)\n proofAssociativity (x::xs) f g | Nil = rewrite proofAssociativity xs f g in Refl\n proofAssociativity (x::xs) f g | (r::rs) = ?holeAssociativity\n"}]}},{"Replacement":{"inode":{"change":5,"pos":13},"path":"src/Data/Either.idr","line":58,"ins":{"up_context":[{"change":5,"pos":1212}],"down_context":[],"flag":"BLOCK","start":2170,"end":2250,"inode":{"change":5,"pos":13}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":1212},"to":{"change":5,"start":1212,"end":1296},"introduced_by":5}],"inode":{"change":5,"pos":13}},"ins_contents":[{"Add":" proofAssociative (Left _) f g = Refl"},{"Add":" proofAssociative (Right _) f g = Refl"}],"del_contents":[{"Del":" proofAssociativity (Left _) f g = Refl\n proofAssociativity (Right _) f g = Refl\n"}]}},{"Edit":{"inode":{"change":5,"pos":117},"path":"src/Data/Boolean.idr","line":4,"atom":{"EdgeMap":{"edges":[{"previous":"","flag":"DELETED","from":{"change":5,"pos":22},"to":{"change":5,"start":207,"end":208},"introduced_by":5},{"previous":"","flag":"DELETED","from":{"change":5,"pos":682},"to":{"change":5,"start":207,"end":208},"introduced_by":5},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":154},"to":{"change":5,"start":207,"end":208},"introduced_by":5},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":208},"to":{"change":5,"start":683,"end":782},"introduced_by":5}],"inode":{"change":5,"pos":117}}},"contents":[{"Del":"\n"},{"Del":"import Algebra.Relation.Equivalence\nimport Algebra.Relation.Preorder\nimport Algebra.Relation.Order\n"}]}},{"Edit":{"inode":{"change":5,"pos":117},"path":"src/Data/Boolean.idr","line":6,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":810},"to":{"change":5,"start":810,"end":838},"introduced_by":5}],"inode":{"change":5,"pos":117}}},"contents":[{"Del":"import Algebra.Group.Monoid\n"}]}},{"Edit":{"inode":{"change":5,"pos":117},"path":"src/Data/Boolean.idr","line":7,"atom":{"NewVertex":{"up_context":[{"change":5,"pos":869}],"down_context":[{"change":5,"pos":140}],"flag":"BLOCK","start":2251,"end":2279,"inode":{"change":5,"pos":117}}},"contents":[{"Add":"import Algebra.Group.Monoid"}]}},{"Edit":{"inode":{"change":5,"pos":117},"path":"src/Data/Boolean.idr","line":12,"atom":{"NewVertex":{"up_context":[{"change":33,"pos":192}],"down_context":[{"change":33,"pos":192}],"flag":"BLOCK","start":2280,"end":2380,"inode":{"change":5,"pos":117}}},"contents":[{"Add":"import Algebra.Relation.Equivalence"},{"Add":"import Algebra.Relation.Preorder"},{"Add":"import Algebra.Relation.Order"},{"Add":""}]}},{"Replacement":{"inode":{"change":5,"pos":117},"path":"src/Data/Boolean.idr","line":157,"ins":{"up_context":[{"change":4,"pos":416}],"down_context":[{"change":4,"pos":460}],"flag":"BLOCK","start":2381,"end":2423,"inode":{"change":5,"pos":117}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":4,"pos":416},"to":{"change":4,"start":416,"end":460},"introduced_by":4}],"inode":{"change":5,"pos":117}},"ins_contents":[{"Add":" proofCommutative = proofDisjCommutative"}],"del_contents":[{"Del":" proofCommutativity = proofDisjCommutative\n"}]}},{"Replacement":{"inode":{"change":5,"pos":117},"path":"src/Data/Boolean.idr","line":162,"ins":{"up_context":[{"change":5,"pos":648}],"down_context":[{"change":5,"pos":681}],"flag":"BLOCK","start":2424,"end":2455,"inode":{"change":5,"pos":117}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":648},"to":{"change":5,"start":648,"end":681},"introduced_by":5}],"inode":{"change":5,"pos":117}},"ins_contents":[{"Add":" proofAssociative False b c ="}],"del_contents":[{"Del":" proofAssociativity False b c =\n"}]}},{"Replacement":{"inode":{"change":5,"pos":117},"path":"src/Data/Boolean.idr","line":166,"ins":{"up_context":[{"change":5,"pos":779}],"down_context":[{"change":4,"pos":477}],"flag":"BLOCK","start":2456,"end":2491,"inode":{"change":5,"pos":117}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":779},"to":{"change":5,"start":779,"end":816},"introduced_by":5}],"inode":{"change":5,"pos":117}},"ins_contents":[{"Add":" proofAssociative True b c = Refl"}],"del_contents":[{"Del":" proofAssociativity True b c = Refl\n"}]}},{"Replacement":{"inode":{"change":5,"pos":117},"path":"src/Data/Boolean.idr","line":220,"ins":{"up_context":[{"change":4,"pos":1181}],"down_context":[{"change":5,"pos":1929}],"flag":"BLOCK","start":2492,"end":2534,"inode":{"change":5,"pos":117}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":4,"pos":1181},"to":{"change":4,"start":1181,"end":1225},"introduced_by":4}],"inode":{"change":5,"pos":117}},"ins_contents":[{"Add":" proofCommutative = proofConjCommutative"}],"del_contents":[{"Del":" proofCommutativity = proofConjCommutative\n"}]}},{"Replacement":{"inode":{"change":5,"pos":117},"path":"src/Data/Boolean.idr","line":224,"ins":{"up_context":[{"change":5,"pos":1482}],"down_context":[{"change":5,"pos":1552}],"flag":"BLOCK","start":2535,"end":2602,"inode":{"change":5,"pos":117}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":1482},"to":{"change":5,"start":1482,"end":1520},"introduced_by":5},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":1520},"to":{"change":5,"start":1814,"end":1847},"introduced_by":5}],"inode":{"change":5,"pos":117}},"ins_contents":[{"Add":" proofAssociative False b c = Refl"},{"Add":" proofAssociative True b c ="}],"del_contents":[{"Del":" proofAssociativity False b c = Refl\n"},{"Del":" proofAssociativity True b c =\n"}]}},{"Replacement":{"inode":{"change":5,"pos":117},"path":"src/Data/Boolean.idr","line":248,"ins":{"up_context":[{"change":5,"pos":371}],"down_context":[{"change":5,"pos":441}],"flag":"BLOCK","start":2603,"end":2665,"inode":{"change":5,"pos":117}},"del":{"edges":[{"previous":"","flag":"DELETED","from":{"change":5,"pos":371},"to":{"change":5,"start":377,"end":441},"introduced_by":5},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":377},"to":{"change":5,"start":377,"end":441},"introduced_by":5}],"inode":{"change":5,"pos":117}},"ins_contents":[{"Add":" proofAssociative = proofAssociative @{BooleanConjSemigroup}"}],"del_contents":[{"Del":" proofAssociative = proofAssociativity @{BooleanConjSemigroup}\n"}]}},{"Replacement":{"inode":{"change":5,"pos":117},"path":"src/Data/Boolean.idr","line":266,"ins":{"up_context":[{"change":5,"pos":373}],"down_context":[{"change":5,"pos":1319}],"flag":"BLOCK","start":2666,"end":2728,"inode":{"change":5,"pos":117}},"del":{"edges":[{"previous":"","flag":"DELETED","from":{"change":5,"pos":373},"to":{"change":5,"start":1255,"end":1319},"introduced_by":5},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":1255},"to":{"change":5,"start":1255,"end":1319},"introduced_by":5}],"inode":{"change":5,"pos":117}},"ins_contents":[{"Add":" proofAssociative = proofAssociative @{BooleanDisjSemigroup}"}],"del_contents":[{"Del":" proofAssociative = proofAssociativity @{BooleanDisjSemigroup}\n"}]}},{"Replacement":{"inode":{"change":5,"pos":2100},"path":"src/Control/IO.idr","line":42,"ins":{"up_context":[{"change":5,"pos":3047}],"down_context":[{"change":5,"pos":3084}],"flag":"BLOCK","start":2729,"end":2764,"inode":{"change":5,"pos":2100}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":3047},"to":{"change":5,"start":3047,"end":3084},"introduced_by":5}],"inode":{"change":5,"pos":2100}},"ins_contents":[{"Add":" proofAssociative = believe_me ()"}],"del_contents":[{"Del":" proofAssociativity = believe_me ()\n"}]}},{"FileAdd":{"meta":{"basename":"Ring","metadata":576},"context":[{"change":5,"pos":10}],"contents":[]}},{"FileAdd":{"meta":{"basename":"Semiring.idr","metadata":0},"context":[{"change":0,"pos":2772}],"contents":[{"Add":"module Algebra.Ring.Semiring"},{"Add":""},{"Add":"import Builtin"},{"Add":""},{"Add":"import Algebra.Group.Magma"},{"Add":"import Algebra.Group.Monoid"},{"Add":""},{"Add":"infixl 5 +"},{"Add":"infixl 6 *"},{"Add":""},{"Add":"public export"},{"Add":"interface Semiring t where"},{"Add":" (+) : t -> t -> t"},{"Add":" (*) : t -> t -> t"},{"Add":""},{"Add":" zero : t"},{"Add":" one : t"},{"Add":""},{"Add":" proofSumZero : (x : t) -> x + zero = x"},{"Add":" proofSumCommutative : (x, y : t) -> x + y = y + x"},{"Add":" proofSumAssociative : (x, y, z : t) -> x + (y + z) = (x + y) + z"},{"Add":""},{"Add":" proofMultOneLeft : (x : t) -> one * x = x"},{"Add":" proofMultOneRight : (x : t) -> x * one = x"},{"Add":" proofMultAssociative : (x, y, z : t) -> x * (y * z) = (x * y) * z"},{"Add":""},{"Add":" proofMultDistributesSumLeft : (x, y, z : t) -> x * (y + z) = x * y + x * z"},{"Add":" proofMultDistributesSumRight : (x, y, z : t) -> (x + y) * z = x * z + y * z"},{"Add":""},{"Add":" zeroAnnihilatorLeft : (x : t) -> zero * x = zero"},{"Add":" zeroAnnihilatorRight : (x : t) -> x * zero = zero"}]}},{"Replacement":{"inode":{"change":5,"pos":639},"path":"src/Algebra/Group/Semigroup.idr","line":11,"ins":{"up_context":[{"change":5,"pos":764}],"down_context":[{"change":4,"pos":1226}],"flag":"BLOCK","start":3599,"end":3667,"inode":{"change":5,"pos":639}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":764},"to":{"change":5,"start":764,"end":834},"introduced_by":5}],"inode":{"change":5,"pos":639}},"ins_contents":[{"Add":" proofAssociative : (x, y, z : t) -> x <> (y <> z) = (x <> y) <> z"}],"del_contents":[{"Del":" proofAssociativity : (x, y, z : t) -> x <> (y <> z) = (x <> y) <> z\n"}]}},{"Replacement":{"inode":{"change":5,"pos":270},"path":"src/Algebra/Group/Magma.idr","line":15,"ins":{"up_context":[{"change":4,"pos":1615}],"down_context":[],"flag":"BLOCK","start":3668,"end":3719,"inode":{"change":5,"pos":270}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":4,"pos":1615},"to":{"change":4,"start":1615,"end":1668},"introduced_by":4}],"inode":{"change":5,"pos":270}},"ins_contents":[{"Add":" proofCommutative : (x, y : t) -> x <> y = y <> x"}],"del_contents":[{"Del":" proofCommutativity : (x, y : t) -> x <> y = y <> x\n"}]}},{"Replacement":{"inode":{"change":5,"pos":12},"path":"src/Algebra/Control/Monad.idr","line":17,"ins":{"up_context":[{"change":5,"pos":1748}],"down_context":[{"change":5,"pos":1749}],"flag":"BLOCK","start":3720,"end":3787,"inode":{"change":5,"pos":12}},"del":{"edges":[{"previous":"","flag":"DELETED","from":{"change":5,"pos":1748},"to":{"change":5,"start":336,"end":405},"introduced_by":5},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":5,"pos":336},"to":{"change":5,"start":336,"end":405},"introduced_by":5}],"inode":{"change":5,"pos":12}},"ins_contents":[{"Add":" proofAssociative : (x : t a) -> (f : a -> t b) -> (g : b -> t c)"}],"del_contents":[{"Del":" proofAssociativity : (x : t a) -> (f : a -> t b) -> (g : b -> t c)\n"}]}}],"owner":"fabian","repo":"veribase-idr2","token":"1y/xLNDDZRjDFuM/DeUqh8MqlYiRV8titBOKjrD5dZA=","login":null}

…

Dependencies

Change contents