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 26–33

independentPersistentCount

Full file
26def independentPersistentCount =
27  (lambda erased slots : Nat .
28    (lambda unrestricted system : (family IndependentStateSystem slots) .
29      (eliminate
30        IndependentStateSystem
31        (lambda unrestricted current : (family IndependentStateSystem slots) . Nat)
32        system
33        (branch IndependentStateSystemOf persistent program initial . persistent))))

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.