From 1d0d45d890e2686b138355829cc09b400a3c1924 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Dec 2016 13:17:10 -0800 Subject: [PATCH] feat(library/init/data/to_string): mark list.to_string as protected --- library/init/data/int/basic.lean | 2 +- library/init/data/to_string.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean index 2c0310bb31..69bb6b82f3 100644 --- a/library/init/data/int/basic.lean +++ b/library/init/data/int/basic.lean @@ -24,7 +24,7 @@ notation `-[1+ ` n `]` := int.neg_succ_of_nat n instance : decidable_eq int := by tactic.mk_dec_eq_instance -private def int.to_string : int → string +protected def int.to_string : int → string | (int.of_nat n) := to_string n | (int.neg_succ_of_nat n) := "-" ++ to_string (succ n) diff --git a/library/init/data/to_string.lean b/library/init/data/to_string.lean index 52cbc0cf8b..7d1a46b9ed 100644 --- a/library/init/data/to_string.lean +++ b/library/init/data/to_string.lean @@ -23,12 +23,12 @@ instance {p : Prop} : has_to_string (decidable p) := -- Remark: type class inference will not consider local instance `b` in the new elaborator ⟨λ b : decidable p, @ite p b _ "tt" "ff"⟩ -def list.to_string_aux {α : Type u} [has_to_string α] : bool → list α → string +protected def list.to_string_aux {α : Type u} [has_to_string α] : bool → list α → string | b [] := "" | tt (x::xs) := to_string x ++ list.to_string_aux ff xs | ff (x::xs) := ", " ++ to_string x ++ list.to_string_aux ff xs -def list.to_string {α : Type u} [has_to_string α] : list α → string +protected def list.to_string {α : Type u} [has_to_string α] : list α → string | [] := "[]" | (x::xs) := "[" ++ list.to_string_aux tt (x::xs) ++ "]"