{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":438660685,"defaultBranch":"main","name":"lisa","ownerLogin":"epfl-lara","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2021-12-15T14:33:35.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/3035238?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1711013193.0","currentOid":""},"activityList":{"items":[{"before":"712da94931109fe02afb828e906a4c83d312a97e","after":"70367a6e85eb906d7e13803a3051a2465ecbb02e","ref":"refs/heads/main","pushedAt":"2024-07-22T09:17:44.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"sankalpgambhir","name":"Sankalp Gambhir","path":"/sankalpgambhir","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10048373?s=80&v=4"},"commit":{"message":"Remove redundant `given Library` leading to compilation error under Scala 3.6+ (#224)","shortMessageHtmlLink":"Remove redundant <code>given Library</code> leading to compilation error under S…"}},{"before":"73a628b775c3205026df2fc5e7ae2919141bfcd8","after":"9976621a9198b3a81aeb1e49a952bc0e232ea491","ref":"refs/heads/itp2024-archive","pushedAt":"2024-06-28T20:22:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"sankalpgambhir","name":"Sankalp Gambhir","path":"/sankalpgambhir","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10048373?s=80&v=4"},"commit":{"message":"Relativize and fix link to examples.","shortMessageHtmlLink":"Relativize and fix link to examples."}},{"before":"cbec1558fa1fcbcaa1a5a5f091f4e933021ebf45","after":"712da94931109fe02afb828e906a4c83d312a97e","ref":"refs/heads/main","pushedAt":"2024-06-18T11:39:48.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"SimonGuilloud","name":null,"path":"/SimonGuilloud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9158556?s=80&v=4"},"commit":{"message":"Dependency and Scala Upgrades (#221)\n\n* More sensible multi line strings, up scalafmt version\r\n\r\n* Upgrade sbt version\r\n\r\n* Upgrade sbt plugins\r\n\r\n* Upgrade Scala version to 3.3.3\r\n\r\n* Update library dependencies\r\n\r\n* Expose library main classes\r\n\r\n* Remove infinite loop (?)\r\n\r\n* Uncomment examples, move Goeland examples to separate object\r\n\r\n* Scala fmt\r\n\r\n* Comment SimpleTautology","shortMessageHtmlLink":"Dependency and Scala Upgrades (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2256329692\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/lisa/issues/221\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/lisa/pull/221/hovercard\" href=\"https://github.com/epfl-lara/lisa/pull/221\">#221</a>)"}},{"before":"b371e3e256dd693fa5588bc2dbe778c0b438de3c","after":"cbec1558fa1fcbcaa1a5a5f091f4e933021ebf45","ref":"refs/heads/main","pushedAt":"2024-04-19T12:33:58.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"SimonGuilloud","name":null,"path":"/SimonGuilloud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9158556?s=80&v=4"},"commit":{"message":"Egraph (#220)\n\nAdd a tactic called \"Congruence\".\r\nThis tactic tries to prove a sequent by congruence.\r\nConsider the congruence closure of all terms and formulas in the sequent, with respect to all === and <=> left of the sequent.\r\nThe sequent is provable by congruence if one of the following conditions is met:\r\n- The right side contains an equality s === t or equivalence a <=> b provable in the congruence closure.\r\n- The left side contains an negated equality !(s === t) or equivalence !(a <=> b) provable in the congruence closure.\r\n- There is a formula a on the left and b on the right such that a and b are congruent.\r\n- There are two formulas a and !b on the left such that a and b are congruent.\r\n- There are two formulas a and !b on the right such that a and b are congruent.\r\n- The sequent is Ol-valid without equality reasoning\r\nNote that complete congruence closure modulo OL is an open problem.\r\n\r\nThe tactic uses an egraph datastructure to compute the congruence closure.\r\nThe egraph itselfs relies on two underlying union-find datastructure, one for terms and one for formulas.\r\nThe union-finds are equiped with an explain method that produces a path between any two elements in the same equivalence class.\r\nEach edge of the path can come from an external equality, or be the consequence of congruence.\r\nThe tactic uses uses this path to produce needed proofs.","shortMessageHtmlLink":"Egraph (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2251701928\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/lisa/issues/220\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/lisa/pull/220/hovercard\" href=\"https://github.com/epfl-lara/lisa/pull/220\">#220</a>)"}},{"before":"0e2b6b700bd8bfa7ff738090b4db2dd0a2f025ff","after":"b371e3e256dd693fa5588bc2dbe778c0b438de3c","ref":"refs/heads/main","pushedAt":"2024-04-18T20:42:23.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"SimonGuilloud","name":null,"path":"/SimonGuilloud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9158556?s=80&v=4"},"commit":{"message":"Type checking and ADTs (#219)\n\nImplements basis of a type system with type checking, ADTs. induction and more.\r\nCo-authored-by: SimonGuilloud <sim-guilloud@bluewin.ch>\r\nCo-authored-by: Simon Guilloud <simon.guilloud@bluewin.ch>\r\nCo-authored-by: Sankalp Gambhir <sankalp.gambhir42@gmail.com>","shortMessageHtmlLink":"Type checking and ADTs (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2237239761\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/lisa/issues/219\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/lisa/pull/219/hovercard\" href=\"https://github.com/epfl-lara/lisa/pull/219\">#219</a>)"}},{"before":"73bc04b9c1176da2110dfc0c6cbcc78ae8194d14","after":"0e2b6b700bd8bfa7ff738090b4db2dd0a2f025ff","ref":"refs/heads/main","pushedAt":"2024-04-08T11:13:08.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"SimonGuilloud","name":null,"path":"/SimonGuilloud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9158556?s=80&v=4"},"commit":{"message":"Support for Goéland and SC-TPTP (#211)\n\nThis adds support for Goéland as a proof tactic, and for parsing of proofs in SC-TPTP format.","shortMessageHtmlLink":"Support for Goéland and SC-TPTP (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2164141123\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/lisa/issues/211\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/lisa/pull/211/hovercard\" href=\"https://github.com/epfl-lara/lisa/pull/211\">#211</a>)"}},{"before":"7414f5354f7af15c8645ef1407b7cead3fd133ae","after":"73a628b775c3205026df2fc5e7ae2919141bfcd8","ref":"refs/heads/itp2024-archive","pushedAt":"2024-04-02T22:30:16.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"agilot","name":"Andrea Gilot","path":"/agilot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/80176994?s=80&v=4"},"commit":{"message":"update adt examples","shortMessageHtmlLink":"update adt examples"}},{"before":"d283c6c9d2e7a01832bb4fe164105e0890edc70a","after":"7414f5354f7af15c8645ef1407b7cead3fd133ae","ref":"refs/heads/itp2024-archive","pushedAt":"2024-03-31T00:50:10.000Z","pushType":"push","commitsCount":6,"pusher":{"login":"sankalpgambhir","name":"Sankalp Gambhir","path":"/sankalpgambhir","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10048373?s=80&v=4"},"commit":{"message":"DEF RED for type instantiation with free vars","shortMessageHtmlLink":"DEF RED for type instantiation with free vars"}},{"before":"960be9ef44bfb28fd9f65ff3b172971d6c9221a3","after":"d283c6c9d2e7a01832bb4fe164105e0890edc70a","ref":"refs/heads/itp2024-archive","pushedAt":"2024-03-29T22:41:00.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"SimonGuilloud","name":null,"path":"/SimonGuilloud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9158556?s=80&v=4"},"commit":{"message":"Merge branch 'itp2024-archive' of github.com:epfl-lara/lisa into itp2024-archive","shortMessageHtmlLink":"Merge branch 'itp2024-archive' of github.com:epfl-lara/lisa into itp2…"}},{"before":"8c9943a397cea2bd7f1e69bbc5cb0a0c836c41b5","after":"960be9ef44bfb28fd9f65ff3b172971d6c9221a3","ref":"refs/heads/itp2024-archive","pushedAt":"2024-03-29T22:08:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"agilot","name":"Andrea Gilot","path":"/agilot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/80176994?s=80&v=4"},"commit":{"message":"Injectivity example ADT","shortMessageHtmlLink":"Injectivity example ADT"}},{"before":"c1881ac708efa1ed61446bb60a6de1ae42f4410c","after":"8c9943a397cea2bd7f1e69bbc5cb0a0c836c41b5","ref":"refs/heads/itp2024-archive","pushedAt":"2024-03-29T21:05:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"agilot","name":"Andrea Gilot","path":"/agilot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/80176994?s=80&v=4"},"commit":{"message":"minor modifications to example","shortMessageHtmlLink":"minor modifications to example"}},{"before":"4a2e05ed54fcba5d9f0aaffddea525a9e4072fa8","after":"c1881ac708efa1ed61446bb60a6de1ae42f4410c","ref":"refs/heads/itp2024-archive","pushedAt":"2024-03-28T10:05:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"agilot","name":"Andrea Gilot","path":"/agilot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/80176994?s=80&v=4"},"commit":{"message":"Edit README and examples","shortMessageHtmlLink":"Edit README and examples"}},{"before":null,"after":"4a2e05ed54fcba5d9f0aaffddea525a9e4072fa8","ref":"refs/heads/types5","pushedAt":"2024-03-21T09:26:33.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"SimonGuilloud","name":null,"path":"/SimonGuilloud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9158556?s=80&v=4"},"commit":{"message":"changed TYPE_INST of abstractions. Need to extends DEF_REF to eliminate TypeInstAbstractionWithout and TypeInstAbstractionWith.","shortMessageHtmlLink":"changed TYPE_INST of abstractions. Need to extends DEF_REF to elimina…"}},{"before":"1da0e3b1faa1be6fa222418d017549d477509bd8","after":"4a2e05ed54fcba5d9f0aaffddea525a9e4072fa8","ref":"refs/heads/itp2024-archive","pushedAt":"2024-03-21T09:22:52.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"SimonGuilloud","name":null,"path":"/SimonGuilloud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9158556?s=80&v=4"},"commit":{"message":"changed TYPE_INST of abstractions. Need to extends DEF_REF to eliminate TypeInstAbstractionWithout and TypeInstAbstractionWith.","shortMessageHtmlLink":"changed TYPE_INST of abstractions. Need to extends DEF_REF to elimina…"}},{"before":"59fc79b496dd4501a8870b472f01670d0ac29fb0","after":"1da0e3b1faa1be6fa222418d017549d477509bd8","ref":"refs/heads/itp2024-archive","pushedAt":"2024-03-20T18:48:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"SimonGuilloud","name":null,"path":"/SimonGuilloud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9158556?s=80&v=4"},"commit":{"message":"bug fixes and improvements","shortMessageHtmlLink":"bug fixes and improvements"}},{"before":"6cc9e16953fe559d6cc13a938d48b68130f779dc","after":"59fc79b496dd4501a8870b472f01670d0ac29fb0","ref":"refs/heads/itp2024-archive","pushedAt":"2024-03-20T12:07:24.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"SimonGuilloud","name":null,"path":"/SimonGuilloud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9158556?s=80&v=4"},"commit":{"message":"untrack metals.sbt","shortMessageHtmlLink":"untrack metals.sbt"}},{"before":"73bc04b9c1176da2110dfc0c6cbcc78ae8194d14","after":"6cc9e16953fe559d6cc13a938d48b68130f779dc","ref":"refs/heads/itp2024-archive","pushedAt":"2024-03-19T10:41:38.000Z","pushType":"pr_merge","commitsCount":94,"pusher":{"login":"sankalpgambhir","name":"Sankalp Gambhir","path":"/sankalpgambhir","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10048373?s=80&v=4"},"commit":{"message":"Merge pull request #217 from sankalpgambhir/itp-merge\n\nHOL implementation + ADTs for ITP 2024 Archive","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2194607172\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/lisa/issues/217\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/lisa/pull/217/hovercard\" href=\"https://github.com/epfl-lara/lisa/pull/217\">#217</a> from sankalpgambhir/itp-merge"}},{"before":null,"after":"73bc04b9c1176da2110dfc0c6cbcc78ae8194d14","ref":"refs/heads/itp2024-archive","pushedAt":"2024-03-19T10:18:16.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"sankalpgambhir","name":"Sankalp Gambhir","path":"/sankalpgambhir","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10048373?s=80&v=4"},"commit":{"message":"Small corrections to Lisa manual (#213)\n\n* Swap 'or' and 'and' in ligature column typo\r\n\r\n* Add missing tautology tactic reference\r\n\r\n* Fix other small typos in manual\r\n\r\n* Fix alignment in kernel chapter\r\n\r\n* Typos in prooflib and set theory\r\n\r\n* Regenerate lisa manual","shortMessageHtmlLink":"Small corrections to Lisa manual (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2165572835\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/lisa/issues/213\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/lisa/pull/213/hovercard\" href=\"https://github.com/epfl-lara/lisa/pull/213\">#213</a>)"}},{"before":"8f68275a8db985a13e4e42b6dd5e75c36108cb68","after":"73bc04b9c1176da2110dfc0c6cbcc78ae8194d14","ref":"refs/heads/main","pushedAt":"2024-03-04T11:57:54.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"SimonGuilloud","name":null,"path":"/SimonGuilloud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9158556?s=80&v=4"},"commit":{"message":"Small corrections to Lisa manual (#213)\n\n* Swap 'or' and 'and' in ligature column typo\r\n\r\n* Add missing tautology tactic reference\r\n\r\n* Fix other small typos in manual\r\n\r\n* Fix alignment in kernel chapter\r\n\r\n* Typos in prooflib and set theory\r\n\r\n* Regenerate lisa manual","shortMessageHtmlLink":"Small corrections to Lisa manual (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2165572835\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/lisa/issues/213\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/lisa/pull/213/hovercard\" href=\"https://github.com/epfl-lara/lisa/pull/213\">#213</a>)"}},{"before":"e27962d9744d3d9ebd94cda2bbbe0032dadb622a","after":"8f68275a8db985a13e4e42b6dd5e75c36108cb68","ref":"refs/heads/main","pushedAt":"2024-03-02T10:51:53.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"SimonGuilloud","name":null,"path":"/SimonGuilloud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9158556?s=80&v=4"},"commit":{"message":"Apply tactic (#212)\n\n* Apply tactic","shortMessageHtmlLink":"Apply tactic (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2164730492\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/lisa/issues/212\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/lisa/pull/212/hovercard\" href=\"https://github.com/epfl-lara/lisa/pull/212\">#212</a>)"}},{"before":"5471d8bda928c703daad51263b79c11969c88a86","after":"e27962d9744d3d9ebd94cda2bbbe0032dadb622a","ref":"refs/heads/main","pushedAt":"2024-02-06T10:51:17.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"SimonGuilloud","name":null,"path":"/SimonGuilloud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9158556?s=80&v=4"},"commit":{"message":"Add option for draft (#207)\n\n* Implement draft option.\r\n\r\nWhile developing proofs and theories, can activate a draft option that will only check the current worked-on file and assume without checking any external theorem. This prevents having to verify the whole library at every run.","shortMessageHtmlLink":"Add option for draft (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2118756882\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/lisa/issues/207\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/lisa/pull/207/hovercard\" href=\"https://github.com/epfl-lara/lisa/pull/207\">#207</a>)"}},{"before":"9dcd3b12e66c4e9c249f604627e1746573c9e5c0","after":"5471d8bda928c703daad51263b79c11969c88a86","ref":"refs/heads/main","pushedAt":"2024-01-09T23:44:26.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"SimonGuilloud","name":null,"path":"/SimonGuilloud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9158556?s=80&v=4"},"commit":{"message":"Lattices2 (#206)\n\nFix README to take the folder change of the reference manual into account. Small improvements to lattices tutorial.","shortMessageHtmlLink":"Lattices2 (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2073281136\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/lisa/issues/206\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/lisa/pull/206/hovercard\" href=\"https://github.com/epfl-lara/lisa/pull/206\">#206</a>)"}},{"before":"fe84b0b5ca4f358797a12b50ec7adb4c603e5cd0","after":"9dcd3b12e66c4e9c249f604627e1746573c9e5c0","ref":"refs/heads/main","pushedAt":"2024-01-09T22:09:10.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"SimonGuilloud","name":null,"path":"/SimonGuilloud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9158556?s=80&v=4"},"commit":{"message":"Small lattices changes (#205)\n\nMinor fix to Lattices tutorial","shortMessageHtmlLink":"Small lattices changes (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2073227660\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/lisa/issues/205\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/lisa/pull/205/hovercard\" href=\"https://github.com/epfl-lara/lisa/pull/205\">#205</a>)"}},{"before":"a60b942bc6b859555703cc68ccabe2aacb937ec8","after":"fe84b0b5ca4f358797a12b50ec7adb4c603e5cd0","ref":"refs/heads/main","pushedAt":"2024-01-08T12:39:22.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"SimonGuilloud","name":null,"path":"/SimonGuilloud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9158556?s=80&v=4"},"commit":{"message":"Lattices (#204)\n\ntypeset lattices example and solutions, improvements to pretty printing","shortMessageHtmlLink":"Lattices (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2070171873\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/lisa/issues/204\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/lisa/pull/204/hovercard\" href=\"https://github.com/epfl-lara/lisa/pull/204\">#204</a>)"}},{"before":"393215c203edb6c1ac25f401f76ed2e45f824f8a","after":"a60b942bc6b859555703cc68ccabe2aacb937ec8","ref":"refs/heads/main","pushedAt":"2024-01-08T11:38:13.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"SimonGuilloud","name":null,"path":"/SimonGuilloud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9158556?s=80&v=4"},"commit":{"message":"Substitution bellow quantifier (#203)\n\n* Add the file CHANGES.md\r\n\r\n* tracking inconsistencies\r\n\r\n* implement a first version of substeq2\r\n\r\n* tracking a bug\r\n\r\n* 2-version works\r\n\r\n* removed all version, renamed versions 2 to normal. All seems to work (including Recursion.scala). Haven't run tests yet, nor tested on function substitutions\r\n\r\n* All tests and the library work. Added sanity checks for substitution steps.\r\n\r\n* Add tests\r\n\r\n* scalafix, scalafmt\r\n\r\n* update CHANGES.md\r\n\r\n* \"of\" for quantified facts has been implemented and tested.\r\n\r\n* manual and changelist updated,  order between forall and free instantiation swapped. scalafix, scalafmt.\r\n\r\n* correct typos","shortMessageHtmlLink":"Substitution bellow quantifier (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2061055304\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/lisa/issues/203\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/lisa/pull/203/hovercard\" href=\"https://github.com/epfl-lara/lisa/pull/203\">#203</a>)"}},{"before":"c627e44dfe1dd9bbf9c728d3acfa32eb86db2f82","after":"393215c203edb6c1ac25f401f76ed2e45f824f8a","ref":"refs/heads/main","pushedAt":"2023-12-28T21:19:58.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"refman is the directory for manul. Style changes and small fixes. (#202)\n\n* refman is the directory for manul. It has a Makefile\r\n\r\n* Format changes (b5, small margin) to reference manual\r\n\r\n* LISA becomes Lisa\r\n\r\n* pull out title page\r\n\r\n* Formatted kernel proof system to fit pages\r\n\r\n* wider margins\r\n\r\n* Fixed reference\r\n\r\n* change margins again. Added text showing margin width with our font is similar to that of LNCS","shortMessageHtmlLink":"refman is the directory for manul. Style changes and small fixes. (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2058663883\" data-permission-text=\"Title is private\" data-url=\"https://github.com/epfl-lara/lisa/issues/202\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/epfl-lara/lisa/pull/202/hovercard\" href=\"https://github.com/epfl-lara/lisa/pull/202\">#202</a>)"}},{"before":"7e381283a4ae35249c6f649410b0f1641c178457","after":"0e61350fe529e70e257a9592a8f3264734b8c5af","ref":"refs/heads/refman","pushedAt":"2023-12-28T21:13:22.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"change margins again. Added text showing margin width with our font is similar to that of LNCS","shortMessageHtmlLink":"change margins again. Added text showing margin width with our font i…"}},{"before":"ebda8999146d9cdfbcbffb9976426162b4128098","after":"7e381283a4ae35249c6f649410b0f1641c178457","ref":"refs/heads/refman","pushedAt":"2023-12-28T20:50:49.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"Fixed reference","shortMessageHtmlLink":"Fixed reference"}},{"before":"a2f10662ff31ee3f54f2fc012f61cb21f8f02513","after":"ebda8999146d9cdfbcbffb9976426162b4128098","ref":"refs/heads/refman","pushedAt":"2023-12-28T20:41:02.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"wider margins","shortMessageHtmlLink":"wider margins"}},{"before":"6b03d5ee87b7b71724dc6c33524aeb5e65bb1e29","after":"a2f10662ff31ee3f54f2fc012f61cb21f8f02513","ref":"refs/heads/refman","pushedAt":"2023-12-28T20:27:21.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"vkuncak","name":"Viktor Kunčak","path":"/vkuncak","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3809719?s=80&v=4"},"commit":{"message":"Formatted kernel proof system to fit pages","shortMessageHtmlLink":"Formatted kernel proof system to fit pages"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEhZN4PgA","startCursor":null,"endCursor":null}},"title":"Activity · epfl-lara/lisa"}