leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: new members

Topic: Sequent calculus


aes_triplex (Jun 12 2019 at 18:37):

Hi all,
I’m a new member. I was wondering if it could be useful to extend the logic library by introducing sequent calculus. Is it?

Simon Hudon (Jun 13 2019 at 19:41):

I think it would be mostly useful if you want to do a deep embedding of some logic into Lean


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll