Lucas Franceschino

Similarly, the following snippet fails with `error[Hacspec]: the variable x_1234 is not present in the context`: ```rust type R = Result::; pub fn h(x: R) -> () { () }...

@pnmadelaine and I are having a quite similar problem, solved by patching `hydra-eval-jobs.cc` in almost the same way you are doing @b-bondurant. In our case, we want Hydra to build...

Thanks @aseemr! I rewrote the desugaring part to use the `sigattrs` field, it is indeed way simpler. However, type checking attributes on sigelt breaks some things: - attributes with universe...

I think this PR is ready now. A few notes about the changes I made recently: - in `Typechecker.Normalize`, `deep_compress` was actually not enough, after testing more thoroughly. So, as...

Nice then :) Yes, sure, I would be glad to!

Hi Nik, Yes, maybe my use case is too specific for this to be added in F*. I'm using this in order to get a "poor man's interactive proving environment"....

Hi, I totally forgot about that PR. I've reworked it so that it passes the CI. I also added a `push_bv_dsenv` to allow parsing and desugaring with given identifiers in...

Hi Benjamin, I think your issue is another form of missed coercion as in #2471, which was fixed by @aseemr yesterday! I tried your example @857b with latest F* master,...

As we were discussing with @TWal and @R1kM, the bug really seems to come (1) from how type inference happens with `eq2` and (2) from unification. Consider the following two...

Hi @tahina-pro, thank you for your answer, I didn't see that note on that wiki page earlier actually, nor issue #2417! Thanks for pointing me to it! Though, I think...