Zulip Chat Archive

Stream: general

Topic: roption and pfun


Yaël Dillies (Aug 03 2021 at 14:23):

Does anyone mind if I split data.pfun in data.option.roption (or data.roption)and data.pfun?

Simon Hudon (Aug 03 2021 at 18:49):

That sounds like a good idea to me

Mario Carneiro (Aug 03 2021 at 20:43):

I suggest using data.roption as the name. Even better, if you are up to it I would really like roption to be renamed to part; my paper on computability theory 3 years ago does this rename and promises that it will eventually be upstreamed but that never happened

Yaël Dillies (Aug 04 2021 at 08:53):

Okay, will do :)

Yaël Dillies (Aug 04 2021 at 08:53):

What's the reasoning behind calling it part? Because of "partial values"? I'm also planning on writing the docstrings.

Yaël Dillies (Aug 04 2021 at 11:46):

There's a clash between your proposed part and computable.part. (See this CI error). What should I do? part is quite a common name, so maybe pvalues or pelems would be better?

Eric Wieser (Aug 04 2021 at 12:02):

It probably makes sense to do the file split before (i.e. as a separate PR) doing any renaming anyway, otherwise the git diff will be lousy

Yaël Dillies (Aug 04 2021 at 12:03):

Sure (I mean you've seen the horrendous diff :stuck_out_tongue_wink:), but the file split is really simple.

Gabriel Ebner (Aug 04 2021 at 12:10):

Yaël Dillies said:

There's a clash between your proposed part and computable.part. (See this CI error). What should I do? part is quite a common name, so maybe pvalues or pelems would be better?

I'm not sure which one you want to rename. I don't think pvalues or pelems is an upgrade over roption. If you want to rename computable.part, then I'd suggest computable.partrec or computable.to_partrec.

Yaël Dillies (Aug 04 2021 at 12:18):

Gabriel Ebner said:

If you want to rename computable.part, then I'd suggest computable.partrec or computable.to_partrec.

Oh yeah, I hadn't paid attention to that but computable.part and computable₂.part really could be called computable.partrec and computable₂.partrec₂, maybe as private lemmas.

Gabriel Ebner (Aug 04 2021 at 12:20):

Why should they be private?

Mario Carneiro (Aug 04 2021 at 12:21):

I agree with renaming part to partrec in those lemmas

Mario Carneiro (Aug 04 2021 at 12:22):

that's just me being too terse for my own good

Mario Carneiro (Aug 04 2021 at 12:22):

not private, they are perfectly normal public lemmas

Yaël Dillies (Aug 04 2021 at 12:33):

Gabriel Ebner said:

Why should they be private?

becausre they will collide with partrec and partrec₂? Or is Lean smart enough to disambiguate?

Yaël Dillies (Aug 04 2021 at 12:46):

Yep, it conflicts.

Yaël Dillies (Aug 04 2021 at 12:47):

If computable.partrec (ex computable.part) is not private, then

theorem of_option {f : α  option β} (hf : computable f) :
  partrec (λ a, (f a : part β)) :=

yields

type mismatch at application
  partrec (λ (a : α), (f a))
term
  λ (a : α), (f a)
has type
  α  part β : Type (max u_1 u_2)
but is expected to have type
  computable ?m_5 : Prop

Mario Carneiro (Aug 04 2021 at 12:48):

oh, you want protected then

Yaël Dillies (Aug 04 2021 at 12:49):

Oh, yeah I meant protected

Mario Carneiro (Aug 04 2021 at 12:50):

that should be fine since it's intended for use with dot notation anyway

Yaël Dillies (Aug 04 2021 at 12:50):

Great! That's what I thought.

Yaël Dillies (Aug 04 2021 at 13:29):

Note that I had to add a few docstrings in data.part because the renaming makes them undocumented in nolints.txt.

Mario Carneiro (Aug 04 2021 at 13:32):

well I'm not going to complain :grinning:

Yaël Dillies (Aug 04 2021 at 13:32):

Yeah I know, docstrings! Terrible


Last updated: Dec 20 2023 at 11:08 UTC