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