Zulip Chat Archive

Stream: new members

Topic: Or Intro Question


view this post on Zulip Rajiv (May 14 2020 at 16:17):

I was wondering if there was a way to specify B, in the expression or.inl x, where x : A, y: B and A B : Prop?

https://leanprover-community.github.io/lean-web-editor/#code=variables%20A%20B%20%3A%20Prop%0A%0Avariable%20x%20%3A%20A%0Avariable%20y%20%3A%20B%0A%0A%23check%20%40or.inl%0A%0A%23check%20or.inl%20x%0A%0A%0A

view this post on Zulip Bhavik Mehta (May 14 2020 at 16:19):

You could do (or.inl x : A ∨ B)

view this post on Zulip Bhavik Mehta (May 14 2020 at 16:20):

or @or.inl A B x

view this post on Zulip Rajiv (May 14 2020 at 16:23):

Thanks @Bhavik Mehta


Last updated: May 11 2021 at 13:22 UTC