max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(init/data/string/basic.lean): inhabited string

Browse source
This commit is contained in:
Daniel Selsam 2016-12-23 15:48:39 -05:00 • committed by Leonardo de Moura
parent a4173467c4
commit 95882c14cd
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/data/string/basic.lean
View file

@ -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 :=