62def runLearningTransition =
63 (lambda erased state : Type 0 .
64 (lambda erased input : Type 0 .
65 (lambda erased output : Type 0 .
66 (lambda unrestricted transition : (family LearningTransition state input output) .
67 (eliminate
68 LearningTransition
69 (lambda unrestricted current : (family LearningTransition state input output) .
70 (pi unrestricted oldState : state . (pi unrestricted observation : input . output)))
71 transition
72 (branch LearningTransitionOf mode replay step . step))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.