Aseem Rastogi

Thanks @mushrm88 for the reporting this, this is indeed counterintuitive. I also expected `make_container` to work smoothly. Here is a smaller version that exhibits the same problem: ``` module Test...

Thanks to @kant2002 for fixing this in #2770.

Thanks @chandradeepdey . An alternate proof for the two lemmas would be using `forall` introduction, rather than repeating the induction. For example, ``` let memP_map_intro_forall (#a #b: Type) (f: (a...

Without looking into why it loops : ), we should add typing hypotheses to the reflection tc APIs. This code would then fail to typecheck, and if we call `must_check`...

Yeah, that should rule it out. E.g., if we had: ``` val core_check_term #u (g:env) (e:term) (t:typ { universe_of g t u }) (eff:tot_or_ghost) : Tac (ret_t (typing_token g e...

Hi @TWal, it has to do with how the `match` in `g` is written: ``` match x with | () -> return () ``` Solver needs to reduce this match...

I was thinking of a different fix. That the first example goes through with ifuel 0 and second with ifuel 1 is intuitive to me. The first one does not...

Hi Clement: It's through the `%.fs-in` targets in makefiles. For example, see the last line here: https://github.com/FStarLang/FStar/blob/master/src/Makefile.boot.common. Most of us have a small script in `.emacs` that finds such a...

That's a good idea, I hadn't thought about that. But in that case, the support will be for all F* files, and not just the typechecker ones, so the code...

You are probably right, I don't know what is a safe value. The way I was thinking it would work is: we would add this `fstar-compute-prover-args-using-make` function to `fstar-mode.el`. Before...