Theorems · Theorem · category theory

PFunctor.M.isubtree.eq_def

∀ {F : PFunctor.{uA, uB}} [inst : DecidableEq F.A] [inst_1 : Inhabited F.M] (x : PFunctor.Approx.Path F) (x_1 : F.M),
  PFunctor.M.isubtree x x_1 =
    match x, x_1 with
    | [], x => x
    | ⟨a, i⟩ :: ps, x => x.casesOn' fun a' f => if h : a = a' then PFunctor.M.isubtree ps (f (cast ⋯ i)) else default

Defined in

Mathlib.Data.PFunctor.Univariate.M

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqInhabited