Sequent calculus

Stream: new members

[aes_triplex]

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]

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