From 82bb37422dce12b0fe16e5ee3f536ce74fe70a17 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 19 Jun 2017 14:30:58 +0200 Subject: [PATCH] fix(library/init/data/int): add to_string instance for integers --- library/init/data/int/basic.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean index 201d294906..4f6d50201c 100644 --- a/library/init/data/int/basic.lean +++ b/library/init/data/int/basic.lean @@ -31,6 +31,9 @@ protected def int.repr : int → string instance : has_repr int := ⟨int.repr⟩ +instance : has_to_string int := +⟨int.repr⟩ + namespace int protected lemma coe_nat_eq (n : ℕ) : ↑n = int.of_nat n := rfl