chore(library/init/meta/name): change notation for mk_str_name

library/init/meta/name.lean

@@ -24,10 +24,7 @@ name.mk_numeral (unsigned.of_nat v) n
 definition mk_simple_name [coercion] (s : string) : name :=
 mk_str_name name.anonymous s
 
-namespace name
-infix ` <s> `:65 := mk_str_name
-infix ` <n> `:65 := mk_num_name
-end name
+infix ` <.> `:65 := mk_str_name
 
 open name
 

tests/lean/run/meta3.lean

@@ -1,5 +1,3 @@
-open name
+check "foo" <.> "bla"
 
-check "foo" <s> "bla"
-
-vm_eval "foo" <s> "bla" <n> 10 <n> 20
+vm_eval mk_num_name ("foo" <.> "bla") 10

tests/lean/run/meta_env1.lean

@@ -41,6 +41,6 @@ vm_eval do
       The new elaborator should be able to handle it.
    -/
    exceptional.success (declaration.type d₁, declaration.type d₂,
-                        environment.is_recursor e₂ ("Two" <s> "rec"),
+                        environment.is_recursor e₂ ("Two" <.> "rec"),
                         environment.constructors_of e₂ "Two",
                         environment.fold e₂ (to_format "") (λ d r, r + format.line + to_fmt (declaration.to_name d)))

tests/lean/run/meta_tac1.lean

@@ -1,6 +1,6 @@
 set_option pp.all true
 
-open tactic name list
+open tactic list
 
 set_option pp.goal.compact true
 set_option pp.binder_types true
@@ -12,10 +12,10 @@ by do env ← get_env,
       assumption
 
 example : ∀ (p : Prop), p → p → p :=
-by do d ← get_decl ("nat" <s> "add"),
+by do d ← get_decl ("nat" <.> "add"),
     trace_expr (declaration.type d),
     trace "nat.rec type:",
-    d ← get_decl ("nat" <s> "rec"),
+    d ← get_decl ("nat" <.> "rec"),
     trace_expr (declaration.type d),
     trace_state,
     r ← result,