nikswamy

Does this help? ``` ;;; fstar-subp-company-backend: init nil ;;;  ;;; Started F* interactive: ("d:/workspace/everest/FStar/bin/fstar.exe" "d:/workspace/everest/FStar/examples/demos/low-star/Test.fst" "--ide" "--smt" "d:/workspace/everest/z3-4.5.1.1f29cebd4df6-x64-win/bin/z3.exe" "--cache_checked_modules" "--use_hints" "--use_hint_hashes" "--use_two_phase_tc" "true" "--use_extracted_interfaces" "--use_two_phase_tc" "true" "--max_fuel" "0" "--max_ifuel" "0")...

Did you mean for the last snippet of fstar-subp-company-backend to replace the previous one? That's what I did and got this ... but the warning didn't show up. Instead, I...

happy to try to collect more data for you, if it helps

Hi Clement. Can you remind me: What's the recommended way to update company? And the recommended way to check which version is currently being used? I installed it again from...

Is anyone still using VimFStar? If so, can we upgrade it to use --ide mode?

Being able to configure C-c C-RET to behave like C-c C-n sounds like a good idea to me. FWIW, finding the end of the current definition is difficult without actually...

@tahina-pro : I'm guessing that you would know the most about this? What's up with our docker images? Do we plan to maintani them or should we just remove them...

We should improve this and when we do also correspondingly update this piece of documentation. https://github.com/FStarLang/PoP-in-FStar/blob/pulse/book/pulse/pulse_conditionals.rst?plain=1#L170-L183

The issue here is that Pulse does not support universe polymorphic definitions. We should at least provide a better error.

I think the problem is because the type of intro_exists is not interpreted properly in Pulse, since it uses a kind of points-free style of specification, which Pulse doesn't expect.