LeanMachineLearning exposition

Learning.IT.step🔗

Minimal Lean file

step🔗

DefinitionLearning.IT.step

Action and feedback at step n.

🔗def
Learning.IT.step.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ) (h : 𝓐 × 𝓨) : 𝓐 × 𝓨
Learning.IT.step.{u_1, u_2} {𝓐 : Type u_1} {𝓨 : Type u_2} (n : ) (h : 𝓐 × 𝓨) : 𝓐 × 𝓨

Code

def step (n : ℕ) (h : ℕ → 𝓐 × 𝓨) : 𝓐 × 𝓨 := h n
Used by (13)

Actions: Source · Open Issue