Zulip Chat Archive
Stream: lean4
Topic: And & Or over Type
Tomas Skrivan (Sep 19 2022 at 09:04):
Is there a reason that classes And and Or are only over Prop? I would like to work with a lattice and have meet and join operations and use the ∧ ∨ notation.
Last updated: Dec 20 2023 at 11:08 UTC