A.1 Core types

Listing A.1: Concept and ConceptClass (Basic.lean)

def Concept (X : Type u) (Y : Type v) := X -> Y

abbrev ConceptClass (X : Type u) (Y : Type v) := Set (Concept X Y)

Listing A.2: BatchLearner (Learner/Core.lean)

structure BatchLearner (X : Type u) (Y : Type v) where
  hypotheses : HypothesisSpace X Y
  learn : {m : N} -> (Fin m -> X * Y) -> Concept X Y
  output_in_H : forall {m : N} (S : Fin m -> X * Y), learn S (*@$\in$@*) hypotheses