Theorems · Definition · category theory

PFunctor.M.isubtree

{F : PFunctor.{uA, uB}} → [DecidableEq F.A] → [Inhabited F.M] → PFunctor.Approx.Path F → F.M → F.M

follow a path through a value of M F and return the subtree found at the end of the path if it is a valid path for that value and return a default tree

Defined in

Mathlib.Data.PFunctor.Univariate.M

Cited by

6 results in Mathlib

Foundations

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

Assumes

DecidableEqInhabited