diff --git a/library/init/meta/name.lean b/library/init/meta/name.lean index a2fdade457..8eae3fa0af 100644 --- a/library/init/meta/name.lean +++ b/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 ` `:65 := mk_str_name -infix ` `:65 := mk_num_name -end name +infix ` <.> `:65 := mk_str_name open name diff --git a/tests/lean/run/meta3.lean b/tests/lean/run/meta3.lean index 256de735ac..7c3b9f25de 100644 --- a/tests/lean/run/meta3.lean +++ b/tests/lean/run/meta3.lean @@ -1,5 +1,3 @@ -open name +check "foo" <.> "bla" -check "foo" "bla" - -vm_eval "foo" "bla" 10 20 +vm_eval mk_num_name ("foo" <.> "bla") 10 diff --git a/tests/lean/run/meta_env1.lean b/tests/lean/run/meta_env1.lean index 9fccfd1534..839acc0141 100644 --- a/tests/lean/run/meta_env1.lean +++ b/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" "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))) diff --git a/tests/lean/run/meta_tac1.lean b/tests/lean/run/meta_tac1.lean index 84adabd122..25d93c3481 100644 --- a/tests/lean/run/meta_tac1.lean +++ b/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" "add"), +by do d ← get_decl ("nat" <.> "add"), trace_expr (declaration.type d), trace "nat.rec type:", - d ← get_decl ("nat" "rec"), + d ← get_decl ("nat" <.> "rec"), trace_expr (declaration.type d), trace_state, r ← result,