You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Minimized from an example from @TWal, somehow we get the error:
* Error 228 at X.fst(16,0-17,26):
- Could not solve typeclass constraint `Type0`
- See also FStar.Tactics.Typeclasses.fst(297,6-300,7)
1 error was reported (see above)
at the entrypoint of tcresolve (this should be clearer btw, the tactics aborts quickly since the goal is not a typeclass constraint, and that should be reflected in the error). Somehow the #_ was expected to have type Type0, instead of usage_type "TLS.SigKey". This incantation makes it work:
Minimized from an example from @TWal, somehow we get the error:
at the entrypoint of tcresolve (this should be clearer btw, the tactics aborts quickly since the goal is not a typeclass constraint, and that should be reflected in the error). Somehow the
#_
was expected to have type Type0, instead ofusage_type "TLS.SigKey"
. This incantation makes it work:The text was updated successfully, but these errors were encountered: