Remove FStar.Ghost.Pull

[gebner]

No description provided.

[TWal]

I am curious why this axiom is removed? Is it because it introduces an unsoundness?

[gebner]

Hi Theophile. There are no concrete plans to pull pull. That's why this PR is marked as draft.

However, pull is one of the few axioms that we include in F* and I have been trying to figure out how much code relies on it. So far I couldn't find anything that makes essential use of pull (see also FStarLang/pulse#291 and project-everest/everparse#160). If you use pull, I'd be curious to learn more.

Is it because it introduces an unsoundness?

I believe that pull is sound. But the negation of pull piqued my interest.

[TWal]

If you use pull, I'd be curious to learn more.

No, I am not using the pull axiom.

I see, if I understand correctly this axiom is convenient, but in practice it can be replaced by something else, so this PR asks the question why we should keep it?

[gebner]

I see, if I understand correctly this axiom is convenient, but in practice it can be replaced by something else, so this PR asks the question why we should keep it?

Apparently, my comment was too opaque then. 😄 I want to add a parametricity axiom to F* that conflicts with pull. If pull was actually used, then that would be a big price to pay. But as this PR shows, we can easily remove pull and make room for this other axiom.

[TWal]

Ah ok, thanks for the explanations!