diff --git a/library/init/lean/parser/reader/module.lean b/library/init/lean/parser/reader/module.lean index 0160a6beff..1a88e2e3b9 100644 --- a/library/init/lean/parser/reader/module.lean +++ b/library/init/lean/parser/reader/module.lean @@ -269,12 +269,6 @@ end reader namespace reader open macro.has_view combinators -instance string_syntax_coe : has_coe string syntax := -⟨λ s, syntax.atom ⟨none, atomic_val.string s⟩⟩ - -instance name_syntax_coe : has_coe name syntax := -⟨λ n, syntax.ident ⟨none, n, none, none⟩⟩ - def mixfix.expand (stx : syntax) : option syntax := do v ← view mixfix stx, syntax.atom ⟨_, atomic_val.string kind⟩ ← pure v.kind | failure, diff --git a/library/init/lean/parser/syntax.lean b/library/init/lean/parser/syntax.lean index 5cbda6866e..88ece48389 100644 --- a/library/init/lean/parser/syntax.lean +++ b/library/init/lean/parser/syntax.lean @@ -55,6 +55,12 @@ inductive syntax instance : inhabited syntax := ⟨syntax.missing⟩ +instance coe_string_syntax : has_coe string syntax := +⟨λ s, syntax.atom ⟨none, atomic_val.string s⟩⟩ + +instance coe_name_syntax : has_coe name syntax := +⟨λ n, syntax.ident ⟨none, n, none, none⟩⟩ + def substring.to_string (s : substring) : string := (s.start.extract s.stop).get_or_else ""