From 95882c14cd8e7c867fa478d5a45f752ad43ea485 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Fri, 23 Dec 2016 15:48:39 -0500 Subject: [PATCH] feat(init/data/string/basic.lean): inhabited string --- library/init/data/string/basic.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean index 415470135b..379758e7b1 100644 --- a/library/init/data/string/basic.lean +++ b/library/init/data/string/basic.lean @@ -12,6 +12,9 @@ def string := list char namespace string @[pattern] def empty : string := list.nil +instance : inhabited string := +⟨empty⟩ + @[pattern] def str : char → string → string := list.cons def concat (a b : string) : string :=