Source/Packages

Learning.Transition

packages/learning/src/Learning/Transition.alpha

72 lines15 declarations2.6 KiBSHA-256 23ecfffa83db

def · lines 62–72

runLearningTransition

Full file
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.