def DY.ALaCarte.Container.decideEquality {CtorId : Type} {ctors : Ctors CtorId} [DecidableEq CtorId] [(id : CtorId) → DecidableEq (ctors id).Data] (x1 x2 : Container ctors) : Decidable (x1 = x2)

Equations

• One or more equations did not get rendered due to their size.

class DY.ALaCarte.RepresentableDecidableEq (f : Type → Type) [FunctorSizeOf f] [Representable f] : Type

• ctorid_deq : DecidableEq (Representable.CtorId f)
• ctor_data_deq (id : Representable.CtorId f) : DecidableEq (Representable.ctors id).Data

@[instance_reducible]

instance DY.ALaCarte.instDecidableEqContainerForOfRepresentableDecidableEq (f : Type → Type) [FunctorSizeOf f] [Representable f] [RepresentableDecidableEq f] : DecidableEq (ContainerFor f)

Equations

• DY.ALaCarte.instDecidableEqContainerForOfRepresentableDecidableEq f = DY.ALaCarte.Container.decideEquality

@[instance_reducible]

instance DY.ALaCarte.instRepresentableDecidableEqFunctorUnionOfDecidableEq {a : Type} [DecidableEq a] (fs : a → Type → Type) [(id : a) → FunctorSizeOf (fs id)] [(id : a) → Representable (fs id)] [(id : a) → RepresentableDecidableEq (fs id)] : RepresentableDecidableEq (FunctorUnion fs)

Equations

• One or more equations did not get rendered due to their size.