Lean module · Frontier
BanditRLProof.Automation
# Automation contracts This file makes the harness roles and artifacts part of the compiled Lean project. It does not run agents; it records the protocol that external agents must satisfy.
Module map
Imports
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
inductive
BanditRLProof.HarnessProfile
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
inductive HarnessProfile where
inductive
BanditRLProof.AgentRole
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
inductive AgentRole where
inductive
BanditRLProof.TaskKind
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
inductive TaskKind where
inductive
BanditRLProof.TaskStatus
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
inductive TaskStatus where
structure
BanditRLProof.ArtifactSpec
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
structure ArtifactSpec where
structure
BanditRLProof.AcceptanceGate
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
structure AcceptanceGate where
structure
BanditRLProof.HarnessTask
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
structure HarnessTask where
def
BanditRLProof.defaultLeanGate
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
def defaultLeanGate : AcceptanceGate where
def
BanditRLProof.defaultHarnessProfile
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
def defaultHarnessProfile : HarnessProfile