Zulip Chat Archive

Stream: new members

Topic: Or Intro Question

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

Bhavik Mehta (May 14 2020 at 16:19):

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

Bhavik Mehta (May 14 2020 at 16:20):

or @or.inl A B x

Rajiv (May 14 2020 at 16:23):

Thanks @Bhavik Mehta

Last updated: Dec 20 2023 at 11:08 UTC