{"header":{"message":"Implement `Algebra.Group` interfaces","description":null,"timestamp":"2021-05-25T02:33:58Z","authors":[{"email":"fabianhjr@protonmail.com","name":"Fabián Heredia Montiel"}]},"hash":"LKG7V6OC5VYTHY3YWWYMIDP5O6OQCWWSMHTMJKALLNQNPOVY375AC","authors":[],"deps":{"hashes":[["LKG7V6OC5VYTHY3YWWYMIDP5O6OQCWWSMHTMJKALLNQNPOVY375AC","Implement `Algebra.Group` interfaces"],["AA",null],["VE7QTPXHFI2SKUADFYESQPELRZZF2JQRPLTFI4TL6J2PALARUO7QC","Add `Algebra.Applicative`"],["6D4TYQRJMN6QEKASHJ3ZN3E7TXF5IEQ3G4ATTZZ5AZC56VXMWFZAC","Add `Algebra.Equivalence`"],["XNPLRKJ4ZK442XNJ5BC7TO3DKXGXFSOSGBZBPW5HZZDHY3IVD6FAC","Init"]],"deps":["VE7QTPXHFI2SKUADFYESQPELRZZF2JQRPLTFI4TL6J2PALARUO7QC"],"known":[]},"hunks":[{"FileAdd":{"meta":{"basename":"Group.idr","metadata":0},"context":[{"change":4,"pos":10}],"contents":[{"Add":"module Algebra.Group"},{"Add":""},{"Add":"import Builtin"},{"Add":""},{"Add":"import public Algebra.Monoid"},{"Add":""},{"Add":"public export"},{"Add":"interface Monoid t => Group t where"},{"Add":" neg : t -> t"},{"Add":" proofLeftInverse : (x : t) -> neg x <> x = Monoid.id"},{"Add":" proofRightInverse : (x : t) -> x <> neg x = Monoid.id"}]}},{"FileAdd":{"meta":{"basename":"Magma.idr","metadata":0},"context":[{"change":4,"pos":10}],"contents":[{"Add":"module Algebra.Magma"},{"Add":""},{"Add":"import Builtin"},{"Add":""},{"Add":"infixl 5 <>"},{"Add":""},{"Add":"public export"},{"Add":"interface Magma t where"},{"Add":" (<>) : t -> t -> t"}]}},{"FileAdd":{"meta":{"basename":"Monoid.idr","metadata":0},"context":[{"change":4,"pos":10}],"contents":[{"Add":"module Algebra.Monoid"},{"Add":""},{"Add":"import Builtin"},{"Add":""},{"Add":"import public Algebra.Semigroup"},{"Add":""},{"Add":"public export"},{"Add":"interface Semigroup t => Monoid t where"},{"Add":" id : t"},{"Add":" proofLeftIdentity : (x : t) -> id <> x = x"},{"Add":" proofRightIdentity : (x : t) -> x <> id = x"}]}},{"FileAdd":{"meta":{"basename":"Semigroup.idr","metadata":0},"context":[{"change":4,"pos":10}],"contents":[{"Add":"module Algebra.Semigroup"},{"Add":""},{"Add":"import Builtin"},{"Add":""},{"Add":"import public Algebra.Magma"},{"Add":""},{"Add":"public export"},{"Add":"interface Magma t => Semigroup t where"},{"Add":" proofAssociativity : (x, y, z : t) -> x <> (y <> z) = (x <> y) <> z"}]}},{"Edit":{"inode":{"change":5,"pos":6174},"path":"veribase.ipkg","line":11,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":640}],"down_context":[{"change":5,"pos":6253}],"flag":"BLOCK","start":835,"end":908,"inode":{"change":5,"pos":6174}}},"contents":[{"Add":"\t, Algebra.Group"},{"Add":"\t, Algebra.Magma"},{"Add":"\t, Algebra.Monoid"},{"Add":"\t, Algebra.Semigroup"}]}}],"owner":"fabian","repo":"veribase-idr2","token":"t4Ez6SZJ5Un10snxa4i+llQhQREzjv+X+zZmnOTCo+M=","login":null}

…

Dependencies

Change contents