Aseem Rastogi

Hi @smoothdeveloper, thanks for submitting this PR. I looked into it a little. I am curious to know why is there an error on your configuration, while all of us...

Closing this issue (see #2747).

Another example from #419, without the annotation on the scrutinee, `path_same_repr` fails. ``` module Test type relation (v: Type) = v → v → Type noeq type path (v: Type)...

Thanks @857b!

We zeroed it down to a normalization call from the unifier that is trying to normalize the types with delta constant 0 as well as zeta on. This results in...

@R1kM, any ideas what's happening here?

Now I remember, I also have seen this kind of thing. Whenever the post assertion depends on the return value, I usually bind the return value explicitly, and then it...

Hi @qaphla , @SECtim , we will need some typechecker changes to support this, and it should be doable without requiring any changes in your code. I will take a...

Hi @SECtim, see this: https://github.com/FStarLang/FStar/pull/2851. You can try this branch. Please feel free to ping me on slack if you see any issues.

PR #2851 adds limited support for extraction of indexed effects. Reification of indexed effects in their full generality is a bigger chunk of work, and we don't plan to address...