nikswamy

We could add `append_mem_auto` to the list library and document this style of usage.

Hi Kirby, I think the DM4Free feature does not handle polymorphic actions like `raise`. We should fail gracefully rather than crashing like this: That's a bug. However, you can workaround...

FYI, this kind of effect index polymorphism is supported using layered effects, but not with DM4F

Thanks! This is an interesting way to visualize the grammar. How would you suggest we use it?

Thanks @mingodad! Already last week I think @amosr mentioned that such documentation is useful and would be a great way to explore and learn F*'s syntax. So, this would be...

Thanks for this fix. I am merging it after offline discussion with @protz ... much appreciated!

I too got this error, after building AxiomProfiler on .NET Framework 4.8 (which is what VS 2022 suggests). Here's the .smt2 file that triggers it. [queries-Alex-1.smt2.txt](https://github.com/viperproject/axiom-profiler/files/10118450/queries-Alex-1.smt2.txt)

Hit this today

Looking at this with @mtzguido It does seem to have something to do with the decreases clauses. We minimized it to: ``` module Test let rec f (x:int) : unit...

hi @TWal Thanks for these examples; they are interesting and revealing. ### Explaining the current behavior Your intuition about the "first pair is free" is not something in my mental...