Cezar Andrici
Cezar Andrici
I updated the main post and added all definitions, thus there are no more assumptions in the PoC. Your previous test failed because previously I did not define the `subcomp`...
Saving here a workaround given by Guido: ``` let ref #a (x : io a) : irepr a (fun p -> forall res. p res) = (fun _ -> x)...
I have this bug too. I try to sign_in a user if it is logged in with CASino and it tries to edit its account,. ``` ruby class RegistrationsController <...
+1 Someone found a solution?
Duplicate of #2210.
This problem does not exists if one uses Arandr instead of Manage Monitors.
A proof of concept of the inversion lemma I would like to prove, but I cannot because of this issue. ```fstar module Inversion type typ = | TUnit : typ...
For what I need, it seems that the situation is even more complicated because the following also don't hold: ```fstar assert (forall a b c d. either a b ==...