{"push_id":1327052671,"size":19,"distinct_size":18,"ref":"refs/heads/nat/lteAddBoth","head":"10ea2ade6e549772a2db6fc73dd6e8e9152c8c67","before":"70af3b769a059e2410db1dcc0a46eb5e588918ec","commits":[{"sha":"8438156c8d229f8410d8addf4cab2eec76c43dfd","author":{"name":"Langston Barrett","email":"3430d393f0b8501c2159c9dd2546c977c4d99f17@gmail.com"},"message":"tutorial: replace \"return\" with \"pure\"","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/8438156c8d229f8410d8addf4cab2eec76c43dfd"},{"sha":"0924f3449b7cb6d366ded56378f6ff175528a7ed","author":{"name":"Adam Schønemann","email":"156b77bb11a533f0db4d9ee1399b0e788c8fbc35@gmail.com"},"message":"Add documentation for the \"with proof\" construct","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/0924f3449b7cb6d366ded56378f6ff175528a7ed"},{"sha":"06bcf51de5e4c69522ece75f828dbd6d30bcea20","author":{"name":"Adam Schønemann","email":"156b77bb11a533f0db4d9ee1399b0e788c8fbc35@gmail.com"},"message":"Add code example and correct the wording","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/06bcf51de5e4c69522ece75f828dbd6d30bcea20"},{"sha":"c9290f9bc6a615349f8e6b33cc143af53c402916","author":{"name":"Langston Barrett","email":"3430d393f0b8501c2159c9dd2546c977c4d99f17@gmail.com"},"message":"docs/tutorial/interfaces.rst: s/return/pure/g","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/c9290f9bc6a615349f8e6b33cc143af53c402916"},{"sha":"01fc7bdbf6cd1fcdbd8e45d2909ad70ab8c5921b","author":{"name":"Apostolis Xekoukoulotakis","email":"741591154d7396be8fb09a399da51d0cd75535f9@gmail.com"},"message":"Correct the module name of TyConInfo.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/01fc7bdbf6cd1fcdbd8e45d2909ad70ab8c5921b"},{"sha":"de5a79c2e460b30ae3ebe3d27d8848f2f8b00030","author":{"name":"Jan de Muijnck-Hughes","email":"b12f6d4f6f80d7d34658089661e60ffcdb5bab59@st-andrews.ac.uk"},"message":"Allow Idris to install IdrisDoc into a central location.\n\n+ Default location is `<getDataDir>/docs`.\n+ Flag `--info` has been updated to show doc location.\n+ New flag `--installdoc <ipkg>` provided to install documentation\n+ New flag `--docdir` provided to show documentation installation location.\n+ New environment variable `IDRIS_DOC_PATH` to allow alternate means of customisation.\n+ Installation for Idris' std libraries has been augmented to install library documentation as well.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/de5a79c2e460b30ae3ebe3d27d8848f2f8b00030"},{"sha":"b949b2846691ef82e679f346a08b78b6af609772","author":{"name":"Jan de Muijnck-Hughes","email":"b12f6d4f6f80d7d34658089661e60ffcdb5bab59@st-andrews.ac.uk"},"message":"Fix build system dir inconsistencies.\n\nThere were several glaring inconsistencies in Idris' paths for system installation. For example, one could override Idris' default data directory, but the system would ignore this for some paths.\nThis commit makes data directory and sub directory access consistent.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/b949b2846691ef82e679f346a08b78b6af609772"},{"sha":"a0d1566ee15702a149f8d4c812496194ddb2d9d3","author":{"name":"Jan de Muijnck-Hughes","email":"b12f6d4f6f80d7d34658089661e60ffcdb5bab59@st-andrews.ac.uk"},"message":"Amended docs and updated CHANGELOG.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/a0d1566ee15702a149f8d4c812496194ddb2d9d3"},{"sha":"10be3da06b711f0f004a852ea450c38e7e732e8a","author":{"name":"David Christiansen","email":"d8099b0f90e53c29d29eb12a7a3caa5af4f12681@davidchristiansen.dk"},"message":"Merge pull request #3461 from xekoukou/master\n\nCorrect the module name of TyConInfo.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/10be3da06b711f0f004a852ea450c38e7e732e8a"},{"sha":"f6fccd7dceaa513bad1f49a04b8e3f0699c94033","author":{"name":"David Christiansen","email":"d8099b0f90e53c29d29eb12a7a3caa5af4f12681@davidchristiansen.dk"},"message":"Merge pull request #3458 from adamschoenemann/patch-1\n\nAdd documentation for the \"with proof\" construct","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/f6fccd7dceaa513bad1f49a04b8e3f0699c94033"},{"sha":"d1eccd8311554091e4b5515e2139d1bd1ed81727","author":{"name":"Jan de Muijnck-Hughes","email":"b12f6d4f6f80d7d34658089661e60ffcdb5bab59@users.noreply.github.com"},"message":"Merge pull request #3462 from jfdm/install-doc-files\n\nAllow Idris to install IdrisDoc into a central location & fix some issues with how paths are overridden.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/d1eccd8311554091e4b5515e2139d1bd1ed81727"},{"sha":"a59677632a47b727f3682ee8d3250d2c48c58b99","author":{"name":"Markus Klink","email":"af940533652c89d62140f8d79d72940d91688e38@inoio.de"},"message":"Remove deprecated calls to return","distinct":false,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/a59677632a47b727f3682ee8d3250d2c48c58b99"},{"sha":"ecc4bb7c0200f1992e1c45214bbe4da48e591bbb","author":{"name":"Jan de Muijnck-Hughes","email":"b12f6d4f6f80d7d34658089661e60ffcdb5bab59@users.noreply.github.com"},"message":"Merge pull request #3464 from justjoheinz/fix/pure\n\nRemove deprecated calls to return","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/ecc4bb7c0200f1992e1c45214bbe4da48e591bbb"},{"sha":"508f4a60ec1d903defc3d320a4c8ff4378fe1b06","author":{"name":"Jan de Muijnck-Hughes","email":"b12f6d4f6f80d7d34658089661e60ffcdb5bab59@st-andrews.ac.uk"},"message":"Merge branch 'fix/tutorial-return' of https://github.com/siddharthist/Idris-dev into siddharthist-fix/tutorial-return","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/508f4a60ec1d903defc3d320a4c8ff4378fe1b06"},{"sha":"43e7ec9c6b7466fd401bef0b36c094e64ef26945","author":{"name":"Jan de Muijnck-Hughes","email":"b12f6d4f6f80d7d34658089661e60ffcdb5bab59@st-andrews.ac.uk"},"message":"Updated remaining use of deprecated `return` in Docs to `pure`.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/43e7ec9c6b7466fd401bef0b36c094e64ef26945"},{"sha":"93772df08ddf57a515b75eb43b8d4e8850a8fbec","author":{"name":"Jan de Muijnck-Hughes","email":"b12f6d4f6f80d7d34658089661e60ffcdb5bab59@st-andrews.ac.uk"},"message":"Merge branch 'siddharthist-fix/tutorial-return'","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/93772df08ddf57a515b75eb43b8d4e8850a8fbec"},{"sha":"be7689bc46aa0b4b47344cb37d4eaddac851206a","author":{"name":"David Christiansen","email":"d8099b0f90e53c29d29eb12a7a3caa5af4f12681@davidchristiansen.dk"},"message":"Make Vect follow the naming convention of List\n\nRename Vect n a to Vect len elem, where it makes sense.","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/be7689bc46aa0b4b47344cb37d4eaddac851206a"},{"sha":"34f466cc2e5be09feb0e6704c223e274f675a507","author":{"name":"Jan de Muijnck-Hughes","email":"b12f6d4f6f80d7d34658089661e60ffcdb5bab59@st-andrews.ac.uk"},"message":"Merge branch 'david-christiansen-coredef'","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/34f466cc2e5be09feb0e6704c223e274f675a507"},{"sha":"10ea2ade6e549772a2db6fc73dd6e8e9152c8c67","author":{"name":"Markus Klink","email":"af940533652c89d62140f8d79d72940d91688e38@inoio.de"},"message":"Add a proof that (p + n) <= (p + m) => n <= m\n\nChanged documentation to use <= instead of <\nAdded total annotation to proofs","distinct":true,"url":"https://api.github.com/repos/justjoheinz/Idris-dev/commits/10ea2ade6e549772a2db6fc73dd6e8e9152c8c67"}]}
{"actor":{"display_login":"justjoheinz"}}