michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/data/string): put is_inhabited theorems on the toplevel

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-10 14:07:20 -08:00
parent f053330755
commit 08a7997a97
1 changed files with 5 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
library/data/string.lean
View file

@ -5,16 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
Module: data.string
Author: Leonardo de Moura
-/
import data.bool
open bool inhabited
open bool
namespace char
protected definition is_inhabited [instance] : inhabited char :=
inhabited.mk (mk ff ff ff ff ff ff ff ff)
end char
protected definition char.is_inhabited [instance] : inhabited char :=
inhabited.mk (char.mk ff ff ff ff ff ff ff ff)
namespace string
protected definition is_inhabited [instance] : inhabited string :=
inhabited.mk empty
end string
protected definition string.is_inhabited [instance] : inhabited string :=
inhabited.mk string.empty