Zulip Chat Archive
Stream: lean4
Topic: unique constituent of the unit
Dean Young (Dec 14 2022 at 18:57):
I'm looking for answers to these two questions in Lean 4:
def point : Unit := ???
def uniqueness : forall (x : Unit), forall (y : Unit), (x = y) := ???
Kevin Buzzard (Dec 14 2022 at 19:25):
You double-posted. Answer here.
Last updated: Dec 20 2023 at 11:08 UTC