tt/ff

Stream: mathlib4

[Johan Commelin]

Mathlib/Data/List/Join.lean:48:-- Porting note: `ff/tt` should be translated to `false/true`.
Mathlib/Data/Num/Basic.lean:83:/-- `bit b n` appends the bit `b` to the end of `n`, where `bit tt x = x1` and `bit ff x = x0`. -/
Mathlib/Data/Num/Basic.lean:267:/-- `bit b n` appends the bit `b` to the end of `n`, where `bit tt x = x1` and `bit ff x = x0`. -/
Mathlib/Init/CcLemmas.lean:64:   cc_config.em is tt. -/
Mathlib/Init/CcLemmas.lean:114:   cc_config.em is tt. -/
Mathlib/Tactic/Ring/Basic.lean:17:Based on <http://www.cs.ru.nl/~freek/courses/tt-2014/read/10.1.1.61.3041.pdf> .
Mathlib/Tactic/Simps/Basic.lean:228:  @[simp] lemma bar_data : ∀ {α : Sort*}, bar.data = tt
Mathlib/Tactic/Simps/Basic.lean:866:  -- cfg.attrs.mapM fun nm ↦ setAttribute nm declName tt -- todo: deal with attributes
Mathlib/Tactic/Simps/Basic.lean:962:          }\{rhsMd := semireducible, simpRhs := tt}."
test/linarith.lean:464:-- by linarith {split_ne := tt}
test/linarith.lean:467:-- by linarith {split_ne := tt}

I think most of these should become true and false, right?

[Ruben Van de Velde]

All except Freek's URL, I think

[Johan Commelin]

Fair enough, I had meant to remove that one

[Eric Wieser]

Also not the porting note at the top

[Johan Commelin]

Apparently docs4#ff_ne_tt is also a thing.

[Johan Commelin]

I haven't found other lemma names that contain ff or tt as an atom.