From fa96fb8deb49c7de8a22705ff5c2749508e86c8e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Jul 2019 16:22:15 -0700 Subject: [PATCH] feat(library/init/lean/position): `HasToString` instance --- library/init/lean/position.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/library/init/lean/position.lean b/library/init/lean/position.lean index f8a9336a92..847a9e1a83 100644 --- a/library/init/lean/position.lean +++ b/library/init/lean/position.lean @@ -26,6 +26,9 @@ protected def lt : Position → Position → Bool instance : HasFormat Position := ⟨fun ⟨l, c⟩ => "⟨" ++ fmt l ++ ", " ++ fmt c ++ "⟩"⟩ +instance : HasToString Position := +⟨fun ⟨l, c⟩ => "⟨" ++ toString l ++ ", " ++ toString c ++ "⟩"⟩ + instance : Inhabited Position := ⟨⟨1, 0⟩⟩ end Position