search

epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

Pair notation and assumeAll #209

Closed sankalpgambhir closed 7 months ago

sankalpgambhir commented 7 months ago
<p>Simple additions, a pair of new extension methods to access pairs as <code>._1</code> and <code>._2</code> and an <code>assumeAll</code> keyword that looks at the LHS of your goal and deconstructs it wrt conjunctions and assumes every discovered formula.</p> </div> </div> <div class="comment"> <div class="user"> <a rel="noreferrer nofollow" target="_blank" href="https://github.com/sankalpgambhir"><img src="https://avatars.githubusercontent.com/u/10048373?v=4" />sankalpgambhir</a> commented <strong> 7 months ago</strong> </div> <div class="markdown-body"> <p>I made some more changes and now they're intertwined with #210 . Better if they just get merged together.</p> </div> </div> <div class="page-bar-simple"> </div> <div class="footer"> <ul class="body"> <li>© <script> document.write(new Date().getFullYear()) </script> Githubissues.</li> <li>Githubissues is a development platform for aggregating issues.</li> </ul> </div> <script src="https://cdn.jsdelivr.net/npm/jquery@3.5.1/dist/jquery.min.js"></script> <script src="/githubissues/assets/js.js"></script> <script src="/githubissues/assets/markdown.js"></script> <script src="https://cdn.jsdelivr.net/gh/highlightjs/cdn-release@11.4.0/build/highlight.min.js"></script> <script src="https://cdn.jsdelivr.net/gh/highlightjs/cdn-release@11.4.0/build/languages/go.min.js"></script> <script> hljs.highlightAll(); </script> </body> </html>