106def digestInitialHash =
107 (eliminate
108 SHA256State
109 (lambda unrestricted current : (family SHA256State) . (family StdList Nat))
110 sha256InitialState
111 (branch
112 SHA256StateValue
113 a
114 b
115 c
116 d
117 e
118 f
119 g
120 h
121 .
122 (constructor
123 StdList
124 StdListCons
125 Nat
126 (modelWord32ToNatural a)
127 (constructor
128 StdList
129 StdListCons
130 Nat
131 (modelWord32ToNatural b)
132 (constructor
133 StdList
134 StdListCons
135 Nat
136 (modelWord32ToNatural c)
137 (constructor
138 StdList
139 StdListCons
140 Nat
141 (modelWord32ToNatural d)
142 (constructor
143 StdList
144 StdListCons
145 Nat
146 (modelWord32ToNatural e)
147 (constructor
148 StdList
149 StdListCons
150 Nat
151 (modelWord32ToNatural f)
152 (constructor
153 StdList
154 StdListCons
155 Nat
156 (modelWord32ToNatural g)
157 (constructor
158 StdList
159 StdListCons
160 Nat
161 (modelWord32ToNatural h)
162 (constructor StdList StdListEmpty Nat)))))))))))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.