@[reducible, inline]

abbrev Tensor2D.Index : Type

Type of tensor dimensions and indexes into tensor dimensions. NOTE: see interaction with linarith where we need to unfold Index into ℕ https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Ergonomics.3A.20linarith.20does.20not.20work.20on.20Nat.20alias/near/365631549

Equations

• Tensor2D.Index = ℕ

structure Tensor2D.Tensor2d' (α : Type) : Type

Tensor2d with existential dimension sizes.

• dim₀ : Tensor2D.Index
• dim₁ : Tensor2D.Index
• mat : Matrix (Fin self.dim₀) (Fin self.dim₁) α

def Tensor2D.Tensor2d'.error (α : Type) : Tensor2D.Tensor2d' α

Equations

• Tensor2D.Tensor2d'.error α = { dim₀ := 0, dim₁ := 0, mat := Matrix.of fun (x _y : Fin 0) => x.elim0 }

def Tensor2D.Tensor2d'.transpose {α : Type} (t : Tensor2D.Tensor2d' α) : Tensor2D.Tensor2d' α

Equations

• t.transpose = { dim₀ := t.dim₁, dim₁ := t.dim₀, mat := t.mat.transpose }

theorem Tensor2D.Tensor2d'.transpose_transpose {α : Type} (t : Tensor2D.Tensor2d' α) : t.transpose.transpose = t

def Tensor2D.Tensor2d'.map {α : Type} {β : Type} (f : α → β) (t : Tensor2D.Tensor2d' α) : Tensor2D.Tensor2d' β

Equations

• Tensor2D.Tensor2d'.map f t = { dim₀ := t.dim₀, dim₁ := t.dim₁, mat := t.mat.map f }

theorem Tensor2D.Tensor2d'.map_functorial {β : Type} {γ : Type} {α : Type} (g : β → γ) (f : α → β) (t : Tensor2D.Tensor2d' α) : Tensor2D.Tensor2d'.map (g ∘ f) t = Tensor2D.Tensor2d'.map g (Tensor2D.Tensor2d'.map f t)

theorem Tensor2D.Tensor2d'.map_error {α : Type} {β : Type} (f : α → β) : Tensor2D.Tensor2d'.map f (Tensor2D.Tensor2d'.error α) = Tensor2D.Tensor2d'.error β

def Tensor2D.const {α : Sort u_1} {β : Sort u_2} (a : α) (_b : β) : α

K combinator / constant function.

Equations

• Tensor2D.const a _b = a

def Tensor2D.Tensor2d'.fill {β : Type} {α : Type} (v : β) (t : Tensor2D.Tensor2d' α) : Tensor2D.Tensor2d' β

Equations

• Tensor2D.Tensor2d'.fill v t = Tensor2D.Tensor2d'.map (Tensor2D.const v) t

def Tensor2D.Tensor2d'.extract {α : Type} (δ₀ : Tensor2D.Index) (δ₁ : Tensor2D.Index) (sz₀ : Tensor2D.Index) (sz₁ : Tensor2D.Index) (t : Tensor2D.Tensor2d' α) : Tensor2D.Tensor2d' α

extract a submatrix of (sz₀ × sz₁) size at offset (δ₀, δ₁). Fails if this is out of bounds.

Equations

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

theorem Tensor2D.Tensor2d'.map_extract {α : Type} {β : Type} (δ₀ : ℕ) (δ₁ : ℕ) (sz₀ : ℕ) (sz₁ : ℕ) (t : Tensor2D.Tensor2d' α) (f : α → β) : Tensor2D.Tensor2d'.extract δ₀ δ₁ sz₀ sz₁ (Tensor2D.Tensor2d'.map f t) = Tensor2D.Tensor2d'.map f (Tensor2D.Tensor2d'.extract δ₀ δ₁ sz₀ sz₁ t)

This implies fill_extract

theorem Tensor2D.Tensor2d'.fill_extract {α : Type} {β : Type} (δ₀ : ℕ) (δ₁ : ℕ) (sz₀ : ℕ) (sz₁ : ℕ) (t : Tensor2D.Tensor2d' α) (v : β) : Tensor2D.Tensor2d'.extract δ₀ δ₁ sz₀ sz₁ (Tensor2D.Tensor2d'.fill v t) = Tensor2D.Tensor2d'.fill v (Tensor2D.Tensor2d'.extract δ₀ δ₁ sz₀ sz₁ t)

inductive Tensor2D.Op : Type

• add: Tensor2D.Op
• constIx: ℕ → Tensor2D.Op
• constTensor: Tensor2D.Tensor2d' ℤ → Tensor2D.Op
• constInt: ℤ → Tensor2D.Op
• sub: Tensor2D.Op
• map2d: Tensor2D.Op
• fill2d: Tensor2D.Op
• extract2d: Tensor2D.Op

inductive Tensor2D.Ty : Type

• int: Tensor2D.Ty
• ix: Tensor2D.Ty
• tensor2d: Tensor2D.Ty

instance Tensor2D.instDecidableEqTy : DecidableEq Tensor2D.Ty

Equations

• Tensor2D.instDecidableEqTy x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Tensor2D.instInhabitedTy : Inhabited Tensor2D.Ty

Equations

• Tensor2D.instInhabitedTy = { default := Tensor2D.Ty.int }

def Tensor2D.Ty.toType : Tensor2D.Ty → Type

Equations

• Tensor2D.Ty.int.toType = ℤ
• Tensor2D.Ty.ix.toType = Tensor2D.Index
• Tensor2D.Ty.tensor2d.toType = Tensor2D.Tensor2d' ℤ

instance Tensor2D.instTyDenoteTy : TyDenote Tensor2D.Ty

Equations

• Tensor2D.instTyDenoteTy = { toType := Tensor2D.Ty.toType }

@[reducible]

def Tensor2D.Op.outTy : Tensor2D.Op → Tensor2D.Ty

Equations

• Tensor2D.Op.add.outTy = Tensor2D.Ty.int
• Tensor2D.Op.sub.outTy = Tensor2D.Ty.int
• (Tensor2D.Op.constIx v).outTy = Tensor2D.Ty.ix
• (Tensor2D.Op.constTensor t).outTy = Tensor2D.Ty.tensor2d
• (Tensor2D.Op.constInt v).outTy = Tensor2D.Ty.int
• Tensor2D.Op.map2d.outTy = Tensor2D.Ty.tensor2d
• Tensor2D.Op.fill2d.outTy = Tensor2D.Ty.tensor2d
• Tensor2D.Op.extract2d.outTy = Tensor2D.Ty.tensor2d

@[reducible]

def Tensor2D.Op.sig : Tensor2D.Op → List Tensor2D.Ty

Equations

• Tensor2D.Op.add.sig = [Tensor2D.Ty.int, Tensor2D.Ty.int]
• Tensor2D.Op.sub.sig = [Tensor2D.Ty.int, Tensor2D.Ty.int]
• (Tensor2D.Op.constIx v).sig = []
• (Tensor2D.Op.constTensor t).sig = []
• (Tensor2D.Op.constInt v).sig = []
• Tensor2D.Op.map2d.sig = [Tensor2D.Ty.tensor2d]
• Tensor2D.Op.fill2d.sig = [Tensor2D.Ty.int, Tensor2D.Ty.tensor2d]
• Tensor2D.Op.extract2d.sig = [Tensor2D.Ty.ix, Tensor2D.Ty.ix, Tensor2D.Ty.ix, Tensor2D.Ty.ix, Tensor2D.Ty.tensor2d]

@[reducible]

def Tensor2D.Op.regSig : Tensor2D.Op → RegionSignature Tensor2D.Ty

Equations

• Tensor2D.Op.map2d.regSig = [([Tensor2D.Ty.int], Tensor2D.Ty.int)]
• x.regSig = []

def Tensor2D.Tensor2D : Dialect

Equations

• Tensor2D.Tensor2D = { Op := Tensor2D.Op, Ty := Tensor2D.Ty, m := Id }

@[reducible]

instance Tensor2D.instDialectSignatureTensor2D : DialectSignature Tensor2D.Tensor2D

Equations

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