{"header":{"message":"Add `Algebra.Applicative`","description":null,"timestamp":"2021-05-24T05:07:33Z","authors":[{"email":"fabianhjr@protonmail.com","name":"Fabián Heredia Montiel"}]},"hash":"VE7QTPXHFI2SKUADFYESQPELRZZF2JQRPLTFI4TL6J2PALARUO7QC","authors":[],"deps":{"hashes":[["VE7QTPXHFI2SKUADFYESQPELRZZF2JQRPLTFI4TL6J2PALARUO7QC","Add `Algebra.Applicative`"],["AA",null],["6D4TYQRJMN6QEKASHJ3ZN3E7TXF5IEQ3G4ATTZZ5AZC56VXMWFZAC","Add `Algebra.Equivalence`"],["XNPLRKJ4ZK442XNJ5BC7TO3DKXGXFSOSGBZBPW5HZZDHY3IVD6FAC","Init"]],"deps":["6D4TYQRJMN6QEKASHJ3ZN3E7TXF5IEQ3G4ATTZZ5AZC56VXMWFZAC"],"known":[]},"hunks":[{"FileAdd":{"meta":{"basename":"Applicative.idr","metadata":0},"context":[{"change":2,"pos":10}],"contents":[{"Add":"module Algebra.Applicative"},{"Add":""},{"Add":"import Builtin"},{"Add":""},{"Add":"import Algebra.Functor"},{"Add":""},{"Add":"%default total"},{"Add":""},{"Add":"infixr 8 <*>"},{"Add":""},{"Add":"public export"},{"Add":"interface Functor t => Applicative t where"},{"Add":" pure : a -> t a"},{"Add":" (<*>) : t (a -> b) -> t a -> t b"},{"Add":""},{"Add":" proofIdentity : (x : t a) -> pure Builtin.identity <*> x = x"},{"Add":" proofComposition : (f : t (a -> b)) -> (g : t (b -> c)) -> (x : t a)"},{"Add":" -> ((pure (.) <*> g) <*> f) <*> x = g <*> f <*> x"},{"Add":" proofHomomorphism : (f : a -> b) -> (x : a) -> pure f <*> pure x = pure (f x)"},{"Add":" proofInterchange : (f : t (a -> b)) -> (x : a) -> f <*> pure x = pure ($ x) <*> f"}]}},{"Edit":{"inode":{"change":4,"pos":6174},"path":"veribase.ipkg","line":8,"atom":{"NewVertex":{"up_context":[{"change":4,"pos":6253}],"down_context":[{"change":2,"pos":2088}],"flag":"BLOCK","start":597,"end":620,"inode":{"change":4,"pos":6174}}},"contents":[{"Add":"\t, Algebra.Applicative"}]}},{"Edit":{"inode":{"change":4,"pos":6174},"path":"veribase.ipkg","line":10,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":2111}],"down_context":[{"change":4,"pos":6253}],"flag":"BLOCK","start":621,"end":640,"inode":{"change":4,"pos":6174}}},"contents":[{"Add":"\t, Algebra.Functor"}]}}],"owner":"fabian","repo":"veribase-idr2","token":"YMI4KCoicL/MQJlLAl1S1U8CUesEYd16dZQIru4jM78=","login":null}

…

Dependencies

Change contents