nikswamy

> So, my claim for .krml is that we always want to extract the entire universe and let KReMLin's reachability analysis decide what matters, rather than making blunt cuts via...

From an offline discussion, @tahina-pro @msprotz and I agreed to the following: We will change the behavior of --extract to match this: > --extract "OCaml:A,B; Kremlin:A,B,C; FSharp:A" etc. with our...

Thanks for the example. I was confronting something similar in the graded monad example here and worked around it by using a slightly different indexing structure: http://fstar-lang.org/tutorial/book/part3/part3_typeclasses.html#beyond-monads-with-do-notation But my workaround...

This program fails with ``` Bug2628.fst(9,2-16,24): (Error 19) could not prove post-condition; The SMT solver could not prove the query, try to spell your proof in more detail or increase...

Thanks for this report and sorry for the slow reply! Things are going wrong because we're misinterpreting the expected arity of the recursive function. This also works: ``` val sort_correct...

@mateuszbujalski : Do you have any advice about this?

Thanks @W95Psp! This looks great and I tried using it a bit and had no problems. One thing that was not clear to me from the comments here is whether...

The issue is that in the current implementation we do not retain the index instantiations, so if the computational behavior of your effect depends on the indices, then we do...

Thanks Amos. 1. `noextract` is confusing and the documentation on the wiki is out of date and should be updated. See this: https://github.com/FStarLang/FStar/pull/2090 `noextract` results in a definition not being...

Adding this pattern to append_mem is indeed fairly natural, but putting it in the standard library will make proofs much more expensive for many clients. Every `mem a (l1 @...