What to call `primrec.not` in mathlib 4

Stream: mathlib4

[Praneeth Kolichala]

In !4#2360, we need to rename the following lemmas:

protected theorem band : primrec₂ band

and

protected theorem and {p q : α → Prop}
  [decidable_pred p] [decidable_pred q]
  (hp : primrec_pred p) (hq : primrec_pred q) :
  primrec_pred (λ a, p a ∧ q a)

Mathport automatically changed band (boolean and is primitive recursive) to and. What should the old and be called? Some ideas:

- And to match Prop (but it is a lemma, not a constructor)
- intersect -- Because it says primrec_pred is closed under intersection
- pand -- current placeholder name to distinguish it from and ("p" for "Prop")
Similarly, the lemmas primrec.not and primrec.or need to be renamed.

[Eric Wieser]

Shouldn't these be in different namespaces?

[Eric Wieser]

docs#primrec.and

[Praneeth Kolichala]

The lemmas band and and are currently both in the primrec namespace. The issue is that Bool.band was renamed to Bool.and, and so, to match this, it seems Primrec.band should become Primrec.and. But then what does the old Primrec.and become?

[Eric Wieser]

Could the Prop version be renamed to primrec_pred.and?