English
If p is a decidable relation and hp is primitive recursive, and f is primitive recursive, then the guarded option function is primitive recursive.
Русский
Если p — распознаваемое отношение, hp примитивно рекурсивно, и f — примитивно рекурсивна, то охраненная опция примитивно рекурсивна.
LaTeX
$$$\\text{option guard} \\{p:\\alpha\\to\\beta\\to\\mathrm{Prop}\\} [DecidableRel p](hp: PrimrecRel p) \\{f: \\alpha\\to\\beta\\} (hf: Primrec f) : Primrec (a \\mapsto \\mathrm{Option.guard}(p(a), f(a)))$$$
Lean4
theorem option_guard {p : α → β → Prop} [DecidableRel p] (hp : PrimrecRel p) {f : α → β} (hf : Primrec f) :
Primrec fun a => Option.guard (p a) (f a) :=
ite (by simpa using hp.comp Primrec.id hf) (option_some_iff.2 hf) (const none)
