search

leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover
Apache License 2.0
232 stars 95 forks source link

chore: deal with nonterminal simps in String/Lemmas #857

Closed semorrison closed 2 months ago

semorrison commented 2 months ago

This file was full on non-terminal simps, and inevitable they started failing and getting in my way when attempting to change @[simp] lemmas in core.

So I've mostly removed the non-terminal simps here.

There are many cases where simp? is giving wrong answers because it is not correctly disambiguating namespaces. I left FIXMEs for all of these rather than doing these by hand.

chabulhwi commented 2 months ago

@semorrison https://github.com/leanprover-community/batteries/pull/864 removes all nonterminal simps from the lemmas that had the FIXME comment.