refactor(library/init/lean/parser): has_tokens default

library/init/lean/parser/basic.lean

@@ -63,8 +63,11 @@ f (f a)
 def tokens (r : ρ) [has_tokens r] :=
 donotinline (has_tokens.tokens r)
 
+instance has_tokens.inhabited (r : ρ) : inhabited (has_tokens r) :=
+⟨⟨[]⟩⟩
+
 instance list.nil.tokens : parser.has_tokens ([] : list ρ) :=
-⟨[]⟩
+default _
 instance list.cons.tokens (r : ρ) (rs : list ρ) [parser.has_tokens r] [parser.has_tokens rs] :
   parser.has_tokens (r::rs) :=
 ⟨tokens r ++ tokens rs⟩

library/init/lean/parser/combinators.lean

@@ -210,7 +210,7 @@ instance dbg.view (r  : parser) (l) [i : parser.has_view r α] : parser.has_view
 {..i}
 
 instance recurse.tokens (α δ m a) [monad_rec α δ m] : parser.has_tokens (recurse a : m δ) :=
-⟨[]⟩ -- recursive use should not contribute any new tokens
+default _ -- recursive use should not contribute any new tokens
 instance recurse.view (α δ m a) [monad_rec α δ m] : parser.has_view (recurse a : m δ) syntax := default _
 
 def with_recurse {α : Type} (init : α) (r : α → rec_t α syntax m syntax) : parser :=

library/init/lean/parser/level.lean

@@ -24,7 +24,7 @@ abbreviation trailing_level_parser := trailing_level_parser_m syntax
 
 /-- Access leading term -/
 def get_leading : trailing_level_parser := read
-instance : has_tokens get_leading := ⟨[]⟩
+instance : has_tokens get_leading := default _
 instance : has_view get_leading syntax := default _
 
 @[derive parser.has_tokens parser.has_view]

library/init/lean/parser/term.lean

@@ -33,7 +33,7 @@ node! term.ident [id: ident.parser, univ: monad_lift ident_univ_spec.parser?]
 namespace term
 /-- Access leading term -/
 def get_leading : trailing_term_parser := read
-instance : has_tokens get_leading := ⟨[]⟩
+instance : has_tokens get_leading := default _
 instance : has_view get_leading syntax := default _
 
 @[derive parser.has_tokens parser.has_view]

library/init/lean/parser/token.lean

@@ -84,7 +84,7 @@ try $ do
   (ss, info) ← with_source_info (as_substring p) trailing_ws,
   pure $ syntax.atom ⟨info, ss.to_string⟩
 
-instance raw.tokens {α} (p : m α) (t) : parser.has_tokens (raw p t : parser) := ⟨[]⟩
+instance raw.tokens {α} (p : m α) (t) : parser.has_tokens (raw p t : parser) := default _
 instance raw.view {α} (p : m α) (t) : parser.has_view (raw p t : parser) syntax := default _
 
 end
@@ -171,7 +171,7 @@ lift $ try $ do {
   pure stx
 } <?> "number"
 
-instance number.tokens : parser.has_tokens (number : parser) := ⟨[]⟩
+instance number.tokens : parser.has_tokens (number : parser) := default _
 instance number.view : parser.has_view (number : parser) syntax := default _
 
 def ident.parser : parser :=
@@ -181,7 +181,7 @@ lift $ try $ do {
   pure stx
 } <?> "identifier"
 
-instance ident.parser.tokens : parser.has_tokens (ident.parser : parser) := ⟨[]⟩
+instance ident.parser.tokens : parser.has_tokens (ident.parser : parser) := default _
 instance ident.parser.view : parser.has_view (ident.parser : parser) syntax := default _
 
 /-- Check if the following token is the symbol _or_ identifier `sym`. Useful for
@@ -208,7 +208,7 @@ lift $ try $ do
   pure stx
 
 instance symbol_or_ident.tokens (sym) : parser.has_tokens (symbol_or_ident sym : parser) :=
-⟨[]⟩
+default _
 instance symbol_or_ident.view (sym) : parser.has_view (symbol_or_ident sym : parser) syntax := default _
 
 end «parser»