Merge pull request #2846 from FStarLang/_aseem_core_equatable

Use leftmost head when checking for equatable symbols in the core typechecker
FStarLang · Mar 9, 2023 · 1c088bc · 1c088bc
2 parents 9594e8f + afaaa11
commit 1c088bc
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 7 deletions.
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml
diff --git a/src/typechecker/FStar.TypeChecker.Core.fst b/src/typechecker/FStar.TypeChecker.Core.fst
@@ -514,8 +514,7 @@ let no_guard (g:result 'a)
       | err -> err
 
 let equatable g t = 
-  let head, _ = U.head_and_args t in
-  Rel.may_relate_with_logical_guard g.tcenv true head
+  t |> U.leftmost_head |> Rel.may_relate_with_logical_guard g.tcenv true
 
 let apply_predicate x p = fun e -> Subst.subst [NT(x.binder_bv, e)] p