AlphaGitHub
Source/Systems

Bob.Prediction

systems/bob/src/Bob/Prediction.alpha

132 lines21 declarations4.9 KiBSHA-256 cb7531dfdc83
Download exact fileView at revision426597bda5753d86c4

def · lines 55–75

bobArgmaxStep

Full file
55def bobArgmaxStep =
56  (lambda unrestricted position : Nat .
57    (lambda unrestricted logit : F32 .
58      (lambda unrestricted state : (family BobArgmaxState) .
59        (eliminate
60          BobArgmaxState
61          (lambda unrestricted current : (family BobArgmaxState) . (family BobArgmaxState))
62          state
63          (branch BobArgmaxEmpty . (constructor BobArgmaxState BobArgmaxValue position logit))
64          (branch
65            BobArgmaxValue
66            bestPosition
67            bestLogit
68            .
69            (nat-eliminate
70              (lambda unrestricted currentIsNotSmaller : Nat . (family BobArgmaxState))
71              (constructor BobArgmaxState BobArgmaxValue bestPosition bestLogit)
72              (lambda unrestricted predecessor : Nat .
73                (lambda unrestricted induction : (family BobArgmaxState) .
74                  (constructor BobArgmaxState BobArgmaxValue position logit)))
75              (naturalIsZero (stdU32LessThan (bobF32OrderKey logit) (bobF32OrderKey bestLogit)))))))))

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.