Leonardo de Moura 0b04376676 refactor(library/init/data/string/basic): mark string implementation as private ... See issue #1175 BTW, we may have to revise this decision in the future when we decide to populate the string library with lemmas. It is inconvenient to prove the lemmas at string/basic.lean since the tactic framework has not been defined yet. Anyway, I think it is worth to keep the private for now, and make sure nobody relies on its implementation.		2017-06-07 18:00:24 -07:00
..
lean	refactor(library/init/data/string/basic): mark string implementation as private	2017-06-07 18:00:24 -07:00
.gitignore	chore(tests/lean,shell/lean): run leantests and leanruntests in parallel	2017-03-30 06:04:00 +02:00