class Isotope.UArgs (Arity : Type uargs) : Type (max uargs (uix + 1))

• Ix : Arity → Type uix

structure Isotope.UArgs.Len (Arity : Type uargs) : Type uargs

• arity : Arity

inductive Isotope.UArgs.Ix? {Arity : Type uargs} [inst : UArgs Arity] : WithZero Arity → Type (max u_1 uargs)

• mk {Arity : Type uargs} [inst : UArgs Arity] {args : Arity} : Ix args → Ix? ↑args

@[implicit_reducible]

instance Isotope.UArgs.instWithZero {Arity : Type uargs} [inst : UArgs Arity] : UArgs (WithZero Arity)

Equations

• Isotope.UArgs.instWithZero = { Ix := fun (args : WithZero Arity) => Isotope.UArgs.Ix? args }

inductive Isotope.UArgs.LIx (Arity : Type u_1) [inst : UArgs Arity] : Type (max u_1 u_2)

• mk {Arity : Type u_1} [inst : UArgs Arity] {args : Arity} : Ix args → LIx Arity

@[implicit_reducible]

instance Isotope.UArgs.instSum {L R : Type uargs} [instL : UArgs L] [instR : UArgs R] : UArgs (L ⊕ R)

Equations

• Isotope.UArgs.instSum = { Ix := fun (e : L ⊕ R) => Sum.elim Isotope.UArgs.Ix Isotope.UArgs.Ix e }

@[implicit_reducible]

instance Isotope.UArgs.instProd {L R : Type uargs} [instL : UArgs L] [instR : UArgs R] : UArgs (L × R)

Equations

• Isotope.UArgs.instProd = { Ix := fun (e : L × R) => Isotope.UArgs.Ix e.1 ⊕ Isotope.UArgs.Ix e.2 }

class Isotope.UArgs.IxFin (Arity : Type uargs) [inst : UArgs Arity] : Type (max u_1 uargs)

• finType (args : Arity) : Fintype (Ix args)

class Isotope.Args (Arity : Type uargs) extends Isotope.UArgs Arity : Type (max (u_1 + 1) uargs)

• Ix : Arity → Type u_1
• posList (args : Arity) : List (Ix args)
• posList_nodup (args : Arity) : (posList args).Nodup
• maxPos : Arity → ℕ
• length_posList_eq_maxPos (args : Arity) : (posList args).length = maxPos args
• ixPos {args : Arity} : Ix args → ℕ
• ixPos_lt_length {args : Arity} (i : Ix args) : ixPos i < (posList args).length
• posList_getElem_ixPos (args : Arity) (i : Ix args) : (posList args)[ixPos i] = i

@[simp]

theorem Isotope.Args.ixPos_lt_maxPos {Arity : Type uargs} [inst : Args Arity] {args : Arity} (i : Ix args) : ixPos i < maxPos args

theorem Isotope.Args.posList_getElem?_ixPos {Arity : Type uargs} [inst : Args Arity] {args : Arity} (i : Ix args) : (posList args)[ixPos i]? = some i

@[simp]

theorem Isotope.Args.mem_posList {Arity : Type uargs} [inst : Args Arity] {args : Arity} (i : Ix args) : i ∈ posList args

@[simp]

theorem Isotope.Args.ixPos_inj {Arity : Type uargs} [inst : Args Arity] {args : Arity} {i j : Ix args} (h : ixPos i = ixPos j) : i = j

theorem Isotope.Args.ixPos_eq_iff {Arity : Type uargs} [inst : Args Arity] {args : Arity} {i j : Ix args} : ixPos i = ixPos j ↔ i = j

@[implicit_reducible]

instance Isotope.Args.ixDecidableEq {Arity : Type uargs} [inst : Args Arity] {args : Arity} : DecidableEq (Ix args)

Equations

• Isotope.Args.ixDecidableEq x✝¹ x✝ = decidable_of_iff (Isotope.Args.ixPos x✝¹ = Isotope.Args.ixPos x✝) ⋯

def Isotope.Args.posFinset {Arity : Type uargs} [inst : Args Arity] (args : Arity) : Finset (Ix args)

Equations

• Isotope.Args.posFinset args = (Isotope.Args.posList args).toFinset

@[simp]

theorem Isotope.Args.posFinset_complete {Arity : Type uargs} [inst : Args Arity] {args : Arity} (i : Ix args) : i ∈ posFinset args

@[implicit_reducible]

instance Isotope.Args.instIxFin {Arity : Type uargs} [inst : Args Arity] : IxFin Arity

Equations

• Isotope.Args.instIxFin = { finType := fun (args : Arity) => { elems := Isotope.Args.posFinset args, complete := ⋯ } }

@[implicit_reducible]

instance Isotope.Args.instNat : Args ℕ

Equations

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

@[implicit_reducible]

instance Isotope.Args.instFin {N : ℕ} : Args (Fin N)

Equations

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

@[implicit_reducible]

instance Isotope.Args.instEmpty : Args Empty

Equations

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

@[implicit_reducible]

instance Isotope.Args.instWithZero {Arity : Type uargs} [inst : Args Arity] : Args (WithZero Arity)

Equations

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

class Isotope.Args.Hom (Src : Type usrc) (Trg : Type utrg) [srcArity : Args Src] [trgArity : Args Trg] : Type (max (max (max u_1 u_2) usrc) utrg)

• mapArgs : Src → Trg
• mapIx {args : Src} : Ix args → Ix (mapArgs args)

@[implicit_reducible]

instance Isotope.Args.Hom.finToNat {N : ℕ} : Hom (Fin N) ℕ

Equations

• Isotope.Args.Hom.finToNat = { mapArgs := fun (n : Fin N) => ↑n, mapIx := fun {args : Fin N} (i : Isotope.UArgs.Ix args) => i }