Source/Packages

Data.SHA256ScheduleExpand

packages/foundation/standard/src/Data/SHA256ScheduleExpand.alpha

376 lines49 declarations14.0 KiBSHA-256 27b122d4be65

def · lines 78–167

sha256LookupScheduleDependencies

Full file
78def sha256LookupScheduleDependencies =
79  (lambda unrestricted schedule : (family SHA256Schedule) .
80    (lambda unrestricted index : Nat .
81      (eliminate
82        SHA256ScheduleLookupResult
83        (lambda unrestricted current : (family SHA256ScheduleLookupResult) .
84          (family SHA256ScheduleDependenciesResult))
85        (sha256ScheduleLookup schedule (naturalSaturatingSubtract index sha256NaturalTwo))
86        (branch
87          SHA256ScheduleLookupSucceeded
88          wordMinus2
89          .
90          (eliminate
91            SHA256ScheduleLookupResult
92            (lambda unrestricted current : (family SHA256ScheduleLookupResult) .
93              (family SHA256ScheduleDependenciesResult))
94            (sha256ScheduleLookup schedule (naturalSaturatingSubtract index sha256NaturalSeven))
95            (branch
96              SHA256ScheduleLookupSucceeded
97              wordMinus7
98              .
99              (eliminate
100                SHA256ScheduleLookupResult
101                (lambda unrestricted current : (family SHA256ScheduleLookupResult) .
102                  (family SHA256ScheduleDependenciesResult))
103                (sha256ScheduleLookup
104                  schedule
105                  (naturalSaturatingSubtract index sha256NaturalFifteen))
106                (branch
107                  SHA256ScheduleLookupSucceeded
108                  wordMinus15
109                  .
110                  (eliminate
111                    SHA256ScheduleLookupResult
112                    (lambda unrestricted current : (family SHA256ScheduleLookupResult) .
113                      (family SHA256ScheduleDependenciesResult))
114                    (sha256ScheduleLookup
115                      schedule
116                      (naturalSaturatingSubtract index sha256NaturalSixteen))
117                    (branch
118                      SHA256ScheduleLookupSucceeded
119                      wordMinus16
120                      .
121                      (constructor
122                        SHA256ScheduleDependenciesResult
123                        SHA256ScheduleDependenciesSucceeded
124                        wordMinus2
125                        wordMinus7
126                        wordMinus15
127                        wordMinus16))
128                    (branch
129                      SHA256ScheduleLookupFailed
130                      error
131                      failedIndex
132                      .
133                      (constructor
134                        SHA256ScheduleDependenciesResult
135                        SHA256ScheduleDependenciesFailed
136                        error
137                        failedIndex))))
138                (branch
139                  SHA256ScheduleLookupFailed
140                  error
141                  failedIndex
142                  .
143                  (constructor
144                    SHA256ScheduleDependenciesResult
145                    SHA256ScheduleDependenciesFailed
146                    error
147                    failedIndex))))
148            (branch
149              SHA256ScheduleLookupFailed
150              error
151              failedIndex
152              .
153              (constructor
154                SHA256ScheduleDependenciesResult
155                SHA256ScheduleDependenciesFailed
156                error
157                failedIndex))))
158        (branch
159          SHA256ScheduleLookupFailed
160          error
161          failedIndex
162          .
163          (constructor
164            SHA256ScheduleDependenciesResult
165            SHA256ScheduleDependenciesFailed
166            error
167            failedIndex)))))

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.