Gabriel Ebner

After giving this some more thought, I don't think we can make the arity version of the attribute work. Knowing the arity is enough to detect this issue, but not...

One more complication: this change by itself increases the verification time of the 3D-generated F* code generated by a lot. As just one data point, verification time of `ELF.fst` soars...

I think we've come to the conclusion that we don't want to do this approach after all. It significantly increases the verification and extraction runtime with the tactic-based normalizer. We're...

Since I didn't see this mentioned either here or at #408, there's the `transfer` tactic that Johannes wrote a long time ago. Here's [an example in mathlib where it transfers...

Check-world found two interesting regressions: 1. The Inria folks like to treat warnings as errors, which breaks now because the warning number changed. 2. The C code produced by Karamel...

Sorry, that wasn't meant negatively at all! The F* library has lots of warnings too, and I agree it would be nicer to avoid them in the first place.

Check-world only reports two regressions now: - dy-star: I believe this is only must_erase_for_extraction vs. erasable. - steel: fixes here: https://github.com/FStarLang/steel/pull/204

This does not fix much without #3665, as effect promotion allows coercion from `unit -> erased nat` to `unit -> GTot (erased nat)` (giving you essentially the same bug). Shelving...

Does this mean that and becomes shortcircuiting? This would be so awesome. ```lean if (← expensive) && (← slow) then -- does not execute `slow` if `expensive` returns false plowSnow...

> This reduces the dependencies that clients take on just for mentioning the char type or a character literal. Currently this brings in a lot to just check a module...