Stream: general

Topic: roption name

Scott Olson (Nov 04 2018 at 10:29):

@Mario Carneiro What's the meaning behind the name of the type roption? Sorry if I'm missing something obvious :p

Mario Carneiro (Nov 04 2018 at 10:29):

I literally forget. I changed the name to part in the recent CPP paper, and I need to update mathlib

Mario Carneiro (Nov 04 2018 at 10:30):

because I didn't want to explain the crazy name

Mario Carneiro (Nov 04 2018 at 10:31):

r is for ... raw? right? no idea

Scott Olson (Nov 04 2018 at 10:32):

haha, fair enough. part does seem clearer. A friend of mine guessed "recursive option"

Simon Hudon (Nov 04 2018 at 18:31):

I seem to recall raw. Maybe in contrast with pfun which has an argument, roption is more minimalist

Last updated: May 12 2021 at 03:23 UTC