Zulip Chat Archive
Stream: new members
Topic: vertical line
Victor Porton (Apr 02 2022 at 02:05):
def option_to_subfunc {α β: Type} (f: α → option β) :
{x : α // option.is_some (f x)} → β | ⟨x, h⟩ := option.get h
I forgot what the vertical line | means.
Victor Porton (Apr 02 2022 at 02:05):
Oh, it is induction.
Last updated: May 02 2025 at 03:31 UTC