test: for flexible reducibility attributes

tests/lean/run/scopedLocalReducibility.lean

@@ -0,0 +1,63 @@
+@[irreducible] def f (x : Nat) := x + 1
+
+/--
+error: type mismatch
+  rfl
+has type
+  f x = f x : Prop
+but is expected to have type
+  f x = x + 1 : Prop
+-/
+#guard_msgs in
+example : f x = x + 1 :=
+  rfl
+
+section
+  attribute [local reducible] f
+  example : f x = x + 1 :=
+    rfl
+end
+
+/--
+error: type mismatch
+  rfl
+has type
+  f x = f x : Prop
+but is expected to have type
+  f x = x + 1 : Prop
+-/
+#guard_msgs in
+example : f x = x + 1 :=
+  rfl
+
+namespace Boo
+  attribute [scoped semireducible] f
+end Boo
+
+/--
+error: type mismatch
+  rfl
+has type
+  f x = f x : Prop
+but is expected to have type
+  f x = x + 1 : Prop
+-/
+#guard_msgs in
+example : f x = x + 1 :=
+  rfl
+
+open Boo in -- `f` should be `semireducible
+example : f x = x + 1 :=
+  rfl
+
+/--
+error: type mismatch
+  rfl
+has type
+  f x = f x : Prop
+but is expected to have type
+  f x = x + 1 : Prop
+-/
+#guard_msgs in
+example : f x = x + 1 :=
+  rfl

tests/pkg/builtin_attr/UserAttr/BlaAttr.lean

@@ -9,3 +9,9 @@ initialize registerBuiltinAttribute {
     descr := "",
     add := fun _ _ _ => pure ()
   }
+
+def myFun (x : Nat) :=
+  x + 1
+
+example : myFun x = x + 1 :=
+  rfl

tests/pkg/builtin_attr/UserAttr/Tst.lean

@@ -2,3 +2,17 @@ import UserAttr.BlaAttr
 
 @[bar] def f (x : Nat) := x + 2
 @[bar] def g (x : Nat) := x + 1
+
+attribute [irreducible] myFun
+
+/--
+error: type mismatch
+  rfl
+has type
+  myFun x = myFun x : Prop
+but is expected to have type
+  myFun x = x + 1 : Prop
+-/
+#guard_msgs in
+example : myFun x = x + 1 :=
+  rfl