nikswamy

The reason inversion on inductives like option is guarded by ifuel is to avoid polluting the solver's context with disjunctions. For single constructor inductives, like tuples, there are no disjunctions---so...

> Of course, for truly "inductive" inductives, like list, omitting the ifuel guard on typing inversion will lead to infinitely many inversions really flooding the context with case splits. @aseemr...

> I guess it would be interesting to test what would happen if the inversion of single-constructor inductives (e.g. tuples, records) were not guarded by ifuel. This is what I'm...

hi @TWal, I have an F* branch `nik_3076` that is green on the F* repo. It removes fuel guards on inversions of single-constructor types. Your examples are captured in `tests/bug-reports/Bug3076.fst`...

That's also a surprise to me ... I do recall that we disable zeta in the bodies of unreduced matches (to prevent loops) but not sure why other delta reduction...

for the moment, i'd be happy to just have a way to suppress these warnings

it seems like disabling company-mode for fstar-mode.el at least made these warnings go away for now.

I created `FStar/examples/demo/low-star/Test.fst` with this content: ``` module Test open Demo.Deps let test l (src dest:lbuffer l uint8) : ST _ _ _ = () ``` And then interacted like...

thank you!

I turned company-mode off, in fstar-enabled-modules and did apply and save. This didn't seem to make the warning go away. But, then I restarted emacs (and checked that company-mode was...