Amos Robinson

Haha! I just ran into this morning and didn't see this issue. Interesting that this feature has been in Mafia for a while, but we all ran into it within...

out of curiosity, does `mafia repl` work? might suffice as a workaround for now

Thanks Nik! The `noextract_to` attribute gets me out of trouble. (I ended up needing both noextract and noextract_to.)

Hi Guido, Yes, this is still useful to me - I haven't been able to find another good way to have precise control over inlining with norm

(Sorry - I actually accidentally pressed the 'merge from master' button. I'll get this building again in the next few days)

Oh, thanks. Good idea - I'll try to make one soon. Do you have a preference whether I put it as a separate PR or modify this one?

Hi Guido, I just thought I'd check - can you think of a robust way to make an automated test that it's not inlining? I noticed that tests/tactics/Inlining.fst says to...

TacticReify.fst: ```fstar module TacticReify module Pure = FStar.Monotonic.Pure module T = FStar.Tactics (* Simple reader-style monad *) type state = unit // -> GTot Type0? let eff_pre = Type0 let...

Hi Guido, I just noticed an issue with pretty-printing after normalising with `nbe` inside a tactic. It looks like a different case to the above, but I thought it looked...

Thanks Guido! Your recent commit works for me (as does `--print_full_names`)