Zulip Chat Archive
Stream: lean4
Topic: parsing optional arguments
Scott Morrison (Sep 14 2022 at 06:18):
If I have a n: Option (TSyntax `num)
, what is the idiomatic way to convert this to a Nat
, by providing a default?
So far I have the rather unpleasant ((n.map (·.1.toNat)).getD 50)
.
Gabriel Ebner (Sep 14 2022 at 07:35):
You can simplify it to n.map (∙.getNat) |>.getD 50
. But I don't think it gets better than that.
Last updated: Dec 20 2023 at 11:08 UTC