Fix some (valid) regressions

FStarLang · Jan 14, 2025 · b93640e · b93640e
1 parent 4953e2b
commit b93640e
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 6 deletions.
diff --git a/tests/micro-benchmarks/BinderAttributes.fst b/tests/micro-benchmarks/BinderAttributes.fst
@@ -9,7 +9,7 @@ let default_to (def : 'a) (x : option 'a) : Tot 'a =
     | None -> def
     | Some a -> a
 
-type description (d : string) = ()
+let description (d : string) = ()
 
 type inductive_example =
     | CaseExplicit : [@@@ description "x"] x:int -> [@@@ description "y"] y:string -> inductive_example

diff --git a/tests/micro-benchmarks/MultipleAttributesBinder.fst b/tests/micro-benchmarks/MultipleAttributesBinder.fst
@@ -7,9 +7,9 @@ type attr_value =
     | String : v:string -> attr_value
     | Int : v:int -> attr_value
 
-type attr1 (v : string) = ()
-type attr2 (v : int) = ()
-type attr3 (v : attr_value) = ()
+let attr1 (v : string) = ()
+let attr2 (v : int) = ()
+let attr3 (v : attr_value) = ()
 
 let f (#[@@@ attr1 "imp"; attr2 1; attr3 (String "x")] x_imp:int) ([@@@ attr1 "exp"; attr2 2; attr3 (String "y")] y:string) : Tot unit =
     ()

diff --git a/tests/micro-benchmarks/RecordFieldAttributes.fst b/tests/micro-benchmarks/RecordFieldAttributes.fst
@@ -2,7 +2,7 @@ module RecordFieldAttributes
 
 module T = FStar.Tactics.V2
 
-type description (d : string) = ()
+let description (d : string) = ()
 
 type r = 
     {

diff --git a/tests/micro-benchmarks/Unit1.Basic.fst b/tests/micro-benchmarks/Unit1.Basic.fst
@@ -219,7 +219,7 @@ let test_skolem_match (x:int) =
   match apply (fun x -> x) 0  with
   | 0 -> 0
 
-type _T = (apply (fun x -> x) 0 = 1)
+type _T = (apply (fun x -> x) 0 == 1)
 
 val test_skolem_refinement: x:int{_T} -> Tot unit
 let test_skolem_refinement x = assert false