roption and pfun

Stream: general

[Yaël Dillies]

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

[Simon Hudon]

That sounds like a good idea to me

[Mario Carneiro]

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]

Okay, will do :)

[Yaël Dillies]

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

[Yaël Dillies]

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]

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]

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

[Gabriel Ebner]

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]

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]

Why should they be private?

[Mario Carneiro]

I agree with renaming part to partrec in those lemmas

[Mario Carneiro]

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

[Mario Carneiro]

not private, they are perfectly normal public lemmas

[Yaël Dillies]

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]

Yep, it conflicts.

[Yaël Dillies]

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]

oh, you want protected then

[Yaël Dillies]

Oh, yeah I meant protected

[Mario Carneiro]

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

[Yaël Dillies]

Great! That's what I thought.

[Yaël Dillies]

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

[Mario Carneiro]

well I'm not going to complain :grinning:

[Yaël Dillies]

Yeah I know, docstrings! Terrible