{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":399570296,"defaultBranch":"master","name":"theorem_proving_in_lean4","ownerLogin":"leanprover","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2021-08-24T18:41:32.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/7233018?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1709322827.0","currentOid":""},"activityList":{"items":[{"before":"9fc001153558257892beca56733821a6a771bf62","after":"bf7dd77bbd401ab9a0a29132619a38f250fe7040","ref":"refs/heads/gh-pages","pushedAt":"2024-05-22T20:02:26.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ leanprover/theorem_proving_in_lean4@cb83ec79ea821d2a3ce2e22595a5ec1a3c8b0d3b 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/cb83ec79ea821d2a3ce2e22595a5ec1a3c8b0d3b/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/cb83ec79ea821d2a3ce2e22595a5ec1a3c8b0d3b\"><tt>cb83ec7</tt></a> 🚀"}},{"before":"81b028359684646f2db48e3909ee81b4fad51dfb","after":"cb83ec79ea821d2a3ce2e22595a5ec1a3c8b0d3b","ref":"refs/heads/master","pushedAt":"2024-05-22T20:02:12.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"david-christiansen","name":"David Thrane Christiansen","path":"/david-christiansen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/115330?s=80&v=4"},"commit":{"message":"Small typos and formatting (#113)","shortMessageHtmlLink":"Small typos and formatting (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2279918623\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/theorem_proving_in_lean4/issues/113\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/theorem_proving_in_lean4/pull/113/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/pull/113\">#113</a>)"}},{"before":"e746df654d8549b69c1d7041e6ebd7572286060d","after":"9fc001153558257892beca56733821a6a771bf62","ref":"refs/heads/gh-pages","pushedAt":"2024-03-01T20:55:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ leanprover/theorem_proving_in_lean4@81b028359684646f2db48e3909ee81b4fad51dfb 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/81b028359684646f2db48e3909ee81b4fad51dfb/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/81b028359684646f2db48e3909ee81b4fad51dfb\"><tt>81b0283</tt></a> 🚀"}},{"before":"985d15effcfbb9bd37e968c877556bcbae662b68","after":"81b028359684646f2db48e3909ee81b4fad51dfb","ref":"refs/heads/master","pushedAt":"2024-03-01T20:54:59.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"david-christiansen","name":"David Thrane Christiansen","path":"/david-christiansen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/115330?s=80&v=4"},"commit":{"message":"indicate how to type `⟨` and `⟩` (#80)\n\n* dependent type theory: indicate how to type anonymous constructor brackets\r\n\r\n---------\r\n\r\nCo-authored-by: David Thrane Christiansen <david@lean-fro.org>","shortMessageHtmlLink":"indicate how to type <code>⟨</code> and <code>⟩</code> (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1951034969\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/theorem_proving_in_lean4/issues/80\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/theorem_proving_in_lean4/pull/80/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/pull/80\">#80</a>)"}},{"before":"0408ffefd1e9442529c8b67512b9c99d9ea97a0d","after":"e746df654d8549b69c1d7041e6ebd7572286060d","ref":"refs/heads/gh-pages","pushedAt":"2024-03-01T20:50:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ leanprover/theorem_proving_in_lean4@985d15effcfbb9bd37e968c877556bcbae662b68 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/985d15effcfbb9bd37e968c877556bcbae662b68/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/985d15effcfbb9bd37e968c877556bcbae662b68\"><tt>985d15e</tt></a> 🚀"}},{"before":"b17956d3064439400889aa3f58260340ef945095","after":"985d15effcfbb9bd37e968c877556bcbae662b68","ref":"refs/heads/master","pushedAt":"2024-03-01T20:49:47.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"david-christiansen","name":"David Thrane Christiansen","path":"/david-christiansen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/115330?s=80&v=4"},"commit":{"message":"fix: tidy up #check output to match Infoview (#89)\n\n* Update quantifiers_and_equality.md correct Infoview\r\n\r\n* Missing #check output\r\n\r\n* @Exists.intro","shortMessageHtmlLink":"fix: tidy up #check output to match Infoview (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2047642804\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/theorem_proving_in_lean4/issues/89\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/theorem_proving_in_lean4/pull/89/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/pull/89\">#89</a>)"}},{"before":"567ee29b96ff6c7192287d79577f5c416a87810d","after":"b17956d3064439400889aa3f58260340ef945095","ref":"refs/heads/master","pushedAt":"2024-03-01T20:47:46.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"david-christiansen","name":"David Thrane Christiansen","path":"/david-christiansen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/115330?s=80&v=4"},"commit":{"message":"fix: typo (#106)","shortMessageHtmlLink":"fix: typo (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2152390549\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/theorem_proving_in_lean4/issues/106\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/theorem_proving_in_lean4/pull/106/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/pull/106\">#106</a>)"}},{"before":"86f187fae4a4479f03fde2dcfa4e80168d834962","after":"0408ffefd1e9442529c8b67512b9c99d9ea97a0d","ref":"refs/heads/gh-pages","pushedAt":"2024-03-01T20:45:50.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ leanprover/theorem_proving_in_lean4@567ee29b96ff6c7192287d79577f5c416a87810d 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/567ee29b96ff6c7192287d79577f5c416a87810d/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/567ee29b96ff6c7192287d79577f5c416a87810d\"><tt>567ee29</tt></a> 🚀"}},{"before":"9ebbfd344dde87b5e0a0ac61835fbc185e993067","after":"567ee29b96ff6c7192287d79577f5c416a87810d","ref":"refs/heads/master","pushedAt":"2024-03-01T20:45:34.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"david-christiansen","name":"David Thrane Christiansen","path":"/david-christiansen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/115330?s=80&v=4"},"commit":{"message":"fix: relative imports are no longer supported in Lean 4 (#90)","shortMessageHtmlLink":"fix: relative imports are no longer supported in Lean 4 (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2057088886\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/theorem_proving_in_lean4/issues/90\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/theorem_proving_in_lean4/pull/90/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/pull/90\">#90</a>)"}},{"before":"7ddc348cdc2d723389ef7f84d9511c21d0d0a1df","after":"86f187fae4a4479f03fde2dcfa4e80168d834962","ref":"refs/heads/gh-pages","pushedAt":"2024-03-01T20:40:26.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ leanprover/theorem_proving_in_lean4@9ebbfd344dde87b5e0a0ac61835fbc185e993067 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/9ebbfd344dde87b5e0a0ac61835fbc185e993067/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/9ebbfd344dde87b5e0a0ac61835fbc185e993067\"><tt>9ebbfd3</tt></a> 🚀"}},{"before":"2d20c140872323d9f0550c3ef3a53770b0fa857a","after":"9ebbfd344dde87b5e0a0ac61835fbc185e993067","ref":"refs/heads/master","pushedAt":"2024-03-01T20:40:12.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"david-christiansen","name":"David Thrane Christiansen","path":"/david-christiansen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/115330?s=80&v=4"},"commit":{"message":"style: replace `@f _ _` with `f` in example (#69)\n\n* style: replace `@f _ _` with `f` in example\r\n\r\nThe `@` is necessary before `euclr` in this example, but nowhere else.\r\nThe current presentation may mislead readers about the effects of `{{ }}` by\r\nmaking them think that it's necessary for `th1` and `th2`.\r\n\r\n* fix: update text to match updated code\r\n\r\n---------\r\n\r\nCo-authored-by: David Thrane Christiansen <david@lean-fro.org>","shortMessageHtmlLink":"style: replace <code>@f _ _</code> with <code>f</code> in example (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1762099175\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/theorem_proving_in_lean4/issues/69\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/theorem_proving_in_lean4/pull/69/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/pull/69\">#69</a>)"}},{"before":"7b3f11480c8619e05aef993025873664b1e35bf6","after":"7ddc348cdc2d723389ef7f84d9511c21d0d0a1df","ref":"refs/heads/gh-pages","pushedAt":"2024-03-01T20:34:30.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ leanprover/theorem_proving_in_lean4@2d20c140872323d9f0550c3ef3a53770b0fa857a 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/2d20c140872323d9f0550c3ef3a53770b0fa857a/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/2d20c140872323d9f0550c3ef3a53770b0fa857a\"><tt>2d20c14</tt></a> 🚀"}},{"before":"048b6bb6a5acdcc8317621ae3d0e14e8a2bc5319","after":"2d20c140872323d9f0550c3ef3a53770b0fa857a","ref":"refs/heads/master","pushedAt":"2024-03-01T20:34:17.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"david-christiansen","name":"David Thrane Christiansen","path":"/david-christiansen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/115330?s=80&v=4"},"commit":{"message":"fix: examples e.g. u not u_1 in some places, to match VS Code (#88)\n\n* Fix examples e.g. u not u_1 in some places, to match VS Code\r\n\r\n* fix: Update to current Lean output\r\n\r\n---------\r\n\r\nCo-authored-by: David Thrane Christiansen <david@lean-fro.org>","shortMessageHtmlLink":"fix: examples e.g. u not u_1 in some places, to match VS Code (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2044028804\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/theorem_proving_in_lean4/issues/88\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/theorem_proving_in_lean4/pull/88/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/pull/88\">#88</a>)"}},{"before":"7116efa6ab35b2f51b8a022936de884572c08790","after":"7b3f11480c8619e05aef993025873664b1e35bf6","ref":"refs/heads/gh-pages","pushedAt":"2024-03-01T20:25:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ leanprover/theorem_proving_in_lean4@048b6bb6a5acdcc8317621ae3d0e14e8a2bc5319 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/048b6bb6a5acdcc8317621ae3d0e14e8a2bc5319/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/048b6bb6a5acdcc8317621ae3d0e14e8a2bc5319\"><tt>048b6bb</tt></a> 🚀"}},{"before":"5f77cc532dfe7a15d26ad50d6205b28b357614d9","after":"048b6bb6a5acdcc8317621ae3d0e14e8a2bc5319","ref":"refs/heads/master","pushedAt":"2024-03-01T20:25:09.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"david-christiansen","name":"David Thrane Christiansen","path":"/david-christiansen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/115330?s=80&v=4"},"commit":{"message":"Update dependent_type_theory.md (#70)\n\nThe `Nat` does not need to be here if this is intended to show that Lean can infer types sometimes.","shortMessageHtmlLink":"Update dependent_type_theory.md (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1787068358\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/theorem_proving_in_lean4/issues/70\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/theorem_proving_in_lean4/pull/70/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/pull/70\">#70</a>)"}},{"before":"8f61ee996ae5d40ab807a30e666f845c87413908","after":"7116efa6ab35b2f51b8a022936de884572c08790","ref":"refs/heads/gh-pages","pushedAt":"2024-03-01T20:22:58.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ leanprover/theorem_proving_in_lean4@5f77cc532dfe7a15d26ad50d6205b28b357614d9 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/5f77cc532dfe7a15d26ad50d6205b28b357614d9/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/5f77cc532dfe7a15d26ad50d6205b28b357614d9\"><tt>5f77cc5</tt></a> 🚀"}},{"before":"b94e413284851aa2693de57344c2218d1cbeb715","after":"5f77cc532dfe7a15d26ad50d6205b28b357614d9","ref":"refs/heads/master","pushedAt":"2024-03-01T20:22:46.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"david-christiansen","name":"David Thrane Christiansen","path":"/david-christiansen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/115330?s=80&v=4"},"commit":{"message":"Update axioms_and_computation.md (#67)\n\ntypo","shortMessageHtmlLink":"Update axioms_and_computation.md (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1722305840\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/theorem_proving_in_lean4/issues/67\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/theorem_proving_in_lean4/pull/67/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/pull/67\">#67</a>)"}},{"before":"d6956b8d89771883bbae7e5bafc779abba44b375","after":"8f61ee996ae5d40ab807a30e666f845c87413908","ref":"refs/heads/gh-pages","pushedAt":"2024-03-01T20:22:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ leanprover/theorem_proving_in_lean4@b94e413284851aa2693de57344c2218d1cbeb715 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/b94e413284851aa2693de57344c2218d1cbeb715/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/b94e413284851aa2693de57344c2218d1cbeb715\"><tt>b94e413</tt></a> 🚀"}},{"before":"f7b08c12b1475a552819bdb52ed6f25b4173e884","after":"d6956b8d89771883bbae7e5bafc779abba44b375","ref":"refs/heads/gh-pages","pushedAt":"2024-03-01T20:22:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ leanprover/theorem_proving_in_lean4@540d39b77b8d4fe267c34be96553fda38faeeb80 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/540d39b77b8d4fe267c34be96553fda38faeeb80/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/540d39b77b8d4fe267c34be96553fda38faeeb80\"><tt>540d39b</tt></a> 🚀"}},{"before":"540d39b77b8d4fe267c34be96553fda38faeeb80","after":"b94e413284851aa2693de57344c2218d1cbeb715","ref":"refs/heads/master","pushedAt":"2024-03-01T20:20:41.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"david-christiansen","name":"David Thrane Christiansen","path":"/david-christiansen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/115330?s=80&v=4"},"commit":{"message":"fix typo in ch 7 (#61)","shortMessageHtmlLink":"fix typo in ch 7 (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1610240847\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/theorem_proving_in_lean4/issues/61\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/theorem_proving_in_lean4/pull/61/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/pull/61\">#61</a>)"}},{"before":"c1dbd1f0719e076079bd42dcb65bf5f6f311ed9f","after":"540d39b77b8d4fe267c34be96553fda38faeeb80","ref":"refs/heads/master","pushedAt":"2024-03-01T20:20:23.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"david-christiansen","name":"David Thrane Christiansen","path":"/david-christiansen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/115330?s=80&v=4"},"commit":{"message":"typo: add -> app (#56)\n\nThe name of the constructor should be `app` rather than `add` according to the context","shortMessageHtmlLink":"typo: add -&gt; app (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1576113592\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/theorem_proving_in_lean4/issues/56\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/theorem_proving_in_lean4/pull/56/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/pull/56\">#56</a>)"}},{"before":"9f0dcae6f9f9bf5aca533b85d8e26f45c7383246","after":"f7b08c12b1475a552819bdb52ed6f25b4173e884","ref":"refs/heads/gh-pages","pushedAt":"2024-03-01T20:19:29.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ leanprover/theorem_proving_in_lean4@c1dbd1f0719e076079bd42dcb65bf5f6f311ed9f 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/c1dbd1f0719e076079bd42dcb65bf5f6f311ed9f/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/c1dbd1f0719e076079bd42dcb65bf5f6f311ed9f\"><tt>c1dbd1f</tt></a> 🚀"}},{"before":"0be40ee27a00c21534267c17388e5ac4800a719a","after":"c1dbd1f0719e076079bd42dcb65bf5f6f311ed9f","ref":"refs/heads/master","pushedAt":"2024-03-01T20:19:16.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"david-christiansen","name":"David Thrane Christiansen","path":"/david-christiansen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/115330?s=80&v=4"},"commit":{"message":"fix: remnants of Lean 3 syntax in induction_and_recursion (#55)","shortMessageHtmlLink":"fix: remnants of Lean 3 syntax in induction_and_recursion (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1533810542\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/theorem_proving_in_lean4/issues/55\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/theorem_proving_in_lean4/pull/55/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/pull/55\">#55</a>)"}},{"before":"8baec1cf5b38e0d3bd544f6b03ef0628b4bd3217","after":"9f0dcae6f9f9bf5aca533b85d8e26f45c7383246","ref":"refs/heads/gh-pages","pushedAt":"2024-03-01T20:11:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ leanprover/theorem_proving_in_lean4@0be40ee27a00c21534267c17388e5ac4800a719a 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/0be40ee27a00c21534267c17388e5ac4800a719a/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/0be40ee27a00c21534267c17388e5ac4800a719a\"><tt>0be40ee</tt></a> 🚀"}},{"before":"43079ad720b6f89404a9da8ca704aa191c1e813f","after":"0be40ee27a00c21534267c17388e5ac4800a719a","ref":"refs/heads/master","pushedAt":"2024-03-01T20:10:46.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"david-christiansen","name":"David Thrane Christiansen","path":"/david-christiansen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/115330?s=80&v=4"},"commit":{"message":"typo: remove duplicated word (#53)","shortMessageHtmlLink":"typo: remove duplicated word (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1473308474\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/theorem_proving_in_lean4/issues/53\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/theorem_proving_in_lean4/pull/53/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/pull/53\">#53</a>)"}},{"before":"bf7a65a94ceb51a08cbea5e45f3e0aad005cb69e","after":"8baec1cf5b38e0d3bd544f6b03ef0628b4bd3217","ref":"refs/heads/gh-pages","pushedAt":"2024-03-01T20:08:20.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ leanprover/theorem_proving_in_lean4@43079ad720b6f89404a9da8ca704aa191c1e813f 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/43079ad720b6f89404a9da8ca704aa191c1e813f/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/43079ad720b6f89404a9da8ca704aa191c1e813f\"><tt>43079ad</tt></a> 🚀"}},{"before":"2baff6f569aeb37cabbb26913d16ee17aae79356","after":"43079ad720b6f89404a9da8ca704aa191c1e813f","ref":"refs/heads/master","pushedAt":"2024-03-01T20:08:05.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"david-christiansen","name":"David Thrane Christiansen","path":"/david-christiansen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/115330?s=80&v=4"},"commit":{"message":"typo: capitalized `list` (#66)","shortMessageHtmlLink":"typo: capitalized <code>list</code> (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1659680302\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/theorem_proving_in_lean4/issues/66\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/theorem_proving_in_lean4/pull/66/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/pull/66\">#66</a>)"}},{"before":"a28a8cfa5787ac84a045c6ee2d98e6d79df459e6","after":"1bf8c579d7572610a16319f8a230772f6002c4a5","ref":"refs/heads/nightly-update","pushedAt":"2024-03-01T19:54:28.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"david-christiansen","name":"David Thrane Christiansen","path":"/david-christiansen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/115330?s=80&v=4"},"commit":{"message":"fix: update examples to work with latest Lean nightly","shortMessageHtmlLink":"fix: update examples to work with latest Lean nightly"}},{"before":null,"after":"a28a8cfa5787ac84a045c6ee2d98e6d79df459e6","ref":"refs/heads/nightly-update","pushedAt":"2024-03-01T19:53:47.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"david-christiansen","name":"David Thrane Christiansen","path":"/david-christiansen","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/115330?s=80&v=4"},"commit":{"message":"fix: Update examples to work with latest Lean nightly","shortMessageHtmlLink":"fix: Update examples to work with latest Lean nightly"}},{"before":"c3e964f696496f40e0be4732df7ee61f7a6c5137","after":"bf7a65a94ceb51a08cbea5e45f3e0aad005cb69e","ref":"refs/heads/gh-pages","pushedAt":"2024-03-01T18:53:18.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"Deploying to gh-pages from @ leanprover/theorem_proving_in_lean4@2baff6f569aeb37cabbb26913d16ee17aae79356 🚀","shortMessageHtmlLink":"Deploying to gh-pages from @ <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/2baff6f569aeb37cabbb26913d16ee17aae79356/hovercard\" href=\"https://github.com/leanprover/theorem_proving_in_lean4/commit/2baff6f569aeb37cabbb26913d16ee17aae79356\"><tt>2baff6f</tt></a> 🚀"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEUVSIfgA","startCursor":null,"endCursor":null}},"title":"Activity · leanprover/theorem_proving_in_lean4"}