Theorems · Theorem · logic and foundations

Primrec.listFilter

∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop} [inst_1 : DecidablePred p],
  PrimrecPred p → Primrec fun L => List.filter (fun x => decide (p x)) L

Filtering a list for elements that satisfy a decidable predicate is primitive recursive.

Defined in

Mathlib.Computability.Primrec.List

Cited by

2 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PrimcodableDecidablePred