max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library/init/lean/parser/{reader/module,syntax}): move new coercions

Browse source
This commit is contained in:
Sebastian Ullrich 2018-08-06 15:05:41 -07:00
parent bf043ab8bd
commit ba7d3ee178
2 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/lean/parser/reader/module.lean
View file

@ -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,

6
library/init/lean/parser/syntax.lean
View file

@ -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 ""