chore: fix tests

tests/compiler/foreign/Main/S.lean

@@ -1,11 +1,11 @@
-constant SPointed : NonemptyType
+opaque SPointed : NonemptyType
 def S : Type := SPointed.type
 instance : Nonempty S := SPointed.property
 
-@[extern "lean_mk_S"] constant mkS (x y : UInt32) (s : @& String) : S
-@[extern "lean_S_add_x_y"] constant S.addXY (s : @& S) : UInt32
-@[extern "lean_S_string"] constant S.string (s : @& S) : String
+@[extern "lean_mk_S"] opaque mkS (x y : UInt32) (s : @& String) : S
+@[extern "lean_S_add_x_y"] opaque S.addXY (s : @& S) : UInt32
+@[extern "lean_S_string"] opaque S.string (s : @& S) : String
 -- The following 3 externs have side effects. Thus, we put them in IO.
-@[extern "lean_S_global_append"] constant appendToGlobalS (str : @& String) : IO Unit
-@[extern "lean_S_global_string"] constant getGlobalString : IO String
-@[extern "lean_S_update_global"] constant updateGlobalS (s : @& S) : IO Unit
+@[extern "lean_S_global_append"] opaque appendToGlobalS (str : @& String) : IO Unit
+@[extern "lean_S_global_string"] opaque getGlobalString : IO String
+@[extern "lean_S_update_global"] opaque updateGlobalS (s : @& S) : IO Unit

tests/lean/248.lean

@@ -1 +1 @@
-@[implementedBy foo] constant foo (x : Nat) : Nat
+@[implementedBy foo] opaque foo (x : Nat) : Nat

tests/lean/248.lean.expected.out

@@ -1 +1 @@
-248.lean:1:30-1:33: error: invalid 'implementedBy' argument 'foo', function cannot be implemented by itself
+248.lean:1:28-1:31: error: invalid 'implementedBy' argument 'foo', function cannot be implemented by itself

tests/lean/Reformat.lean.expected.out

@@ -316,3 +316,4 @@ instance {α : Type u} [DecidableEq α] : BEq α :=
 @[macroInline]
 def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : Not c → α) : α :=
   Decidable.casesOn (motive := fun _ => α) h e t
+

tests/lean/interactive/hover.lean.expected.out

@@ -98,10 +98,10 @@ null
   "end": {"line": 107, "character": 17}},
  "contents": {"value": "```lean\nfoo : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
- "position": {"line": 112, "character": 9}}
+ "position": {"line": 112, "character": 7}}
 {"range":
- {"start": {"line": 112, "character": 9},
-  "end": {"line": 112, "character": 12}},
+ {"start": {"line": 112, "character": 7},
+  "end": {"line": 112, "character": 10}},
  "contents": {"value": "```lean\nBar.foo : Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 115, "character": 9}}

tests/lean/multiConstantError.lean.expected.out

@@ -1,6 +1,6 @@
+multiConstantError.lean:1:9-1:10: error: failed to infer binder type
+recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`
 multiConstantError.lean:1:11-1:12: error: failed to infer binder type
 recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`
-multiConstantError.lean:1:13-1:14: error: failed to infer binder type
-recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`
-multiConstantError.lean:3:11-3:12: error: failed to infer binder type
+multiConstantError.lean:3:9-3:10: error: failed to infer binder type
 recall that you cannot declare multiple constants in a single declaration. The identifier(s) `α`, `β` are being interpreted as parameters `(α : _)`, `(β : _)`

tests/lean/run/impByNameResolution.lean

@@ -1,9 +1,9 @@
-
+--
 
 namespace Foo
 
 def f (x : Nat) : Nat := x + 1
 
-@[implementedBy f] constant g : Nat → Nat
+@[implementedBy f] opaque g : Nat → Nat
 
 end Foo

tests/lean/run/unsafeConst.lean

@@ -1 +1 @@
-@[extern "foo"] unsafe constant something : α
+@[extern "foo"] unsafe opaque something : α

tests/lean/sanitychecks.lean.expected.out

@@ -6,7 +6,7 @@ structural recursion cannot be used
 well-founded recursion cannot be used, 'unsound' does not take any (non-fixed) arguments
 sanitychecks.lean:4:8-5:10: error: 'partial' theorems are not allowed, 'partial' is a code generation directive
 sanitychecks.lean:7:7-8:10: error: 'unsafe' theorems are not allowed
-sanitychecks.lean:10:0-10:25: error: failed to synthesize
+sanitychecks.lean:10:0-10:23: error: failed to synthesize
   Inhabited False
 sanitychecks.lean:18:12-18:20: error: invalid use of 'partial', 'Foo.unsound3' is not a function
   False