AlphaGitHub
Source/Packages

Learning.IndependentState

packages/learning/src/Learning/IndependentState.alpha

143 lines10 declarations5.7 KiBSHA-256 8f18c85bfe35
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 45–53

independentInitialValues

Full file
45def independentInitialValues =
46  (lambda erased slots : Nat .
47    (lambda unrestricted system : (family IndependentStateSystem slots) .
48      (eliminate
49        IndependentStateSystem
50        (lambda unrestricted current : (family IndependentStateSystem slots) .
51          (family StdList (family StdList StdU64)))
52        system
53        (branch IndependentStateSystemOf persistent program initial . initial))))

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.