GridWorld Artifact Positions

Shared JSON encoding for GridWorld coordinates used by policy/path visualization artifacts. Positions are stored as [row, col] pairs because that format is compact, human-readable, and easy for the widgets to consume.

def Runtime.RL.Artifacts.GridWorld.posToJson (p : Nat × Nat) : Lean.Json

Encode a GridWorld position (row, col) as JSON [row, col].

def Runtime.RL.Artifacts.GridWorld.posOfJsonE (field : String) (j : Lean.Json) : Except String (Nat × Nat)

Decode a GridWorld position (row, col) from JSON [row, col].

The field argument is only used for nicer error messages.

def Runtime.RL.Artifacts.GridWorld.posArrayToJson (xs : Array (Nat × Nat)) : Lean.Json

Encode an array of GridWorld positions as a JSON array of [row, col] pairs.

def Runtime.RL.Artifacts.GridWorld.posArrayOfJsonE (field : String) (j : Lean.Json) : Except String (Array (Nat × Nat))

Decode an array of GridWorld positions from JSON, using field only for nicer errors.