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
module FStar.Preorder
type relation (a : Type) = a -> a -> Type0
let reflexive (#a:Type) (rel:relation a) =
forall (x:a). rel x x
Hover over relation inside reflective declaration. LSP crash consistently
/home/kant/d/github/fstar/FStar/ulib/FStar.Preorder.fst(22,29-22,37): (Warning 264) Normalization failed with error FStar_Errors.Error(_)
(Warning 282) Expected Z3 version "Z3 version 4.8.5", got "Z3 version 4.8.15 - 64 bit
"
Please download the version of Z3 corresponding to your platform from:
https://github.com/FStarLang/binaries/tree/master/z3-tested
and add the bin/ subdirectory into your PATH
(Error 334) Internal error: incompatible version for universe unification variable ?3: current version is 8.0; got version 2.1
The text was updated successfully, but these errors were encountered:
Consider this module
Hover over
relation
insidereflective
declaration. LSP crash consistentlyThe text was updated successfully, but these errors were encountered: