fix(library/init/data/int): add to_string instance for integers
This commit is contained in:
parent
981f439de5
commit
82bb37422d
1 changed files with 3 additions and 0 deletions
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue