Operations from a declared fragment and individually declared operations
share scope and repeat-flow admission; preserving an error identity must not
introduce a second, more permissive path into recorder-private storage.
213def nativeObservedAdmitOperation =
214 (lambda unrestricted applicationBytes : Nat .
215 (lambda unrestricted applicationSlots : Nat .
216 (lambda unrestricted operation : (family NativePhysicalOperation) .
217 (lambda unrestricted induction : (pi unrestricted depth : Nat . (pi unrestricted closed : Nat . Nat)) .
218 (lambda unrestricted depth : Nat .
219 (lambda unrestricted closed : Nat .
220 (naturalAnd
221 (nativeObservedOperationAllowed operation)
222 (naturalAnd
223 (nativePhysicalOperationScopeAdmission
224 applicationBytes
225 applicationSlots
226 operation)
227 (naturalAnd
228 (naturalOr
229 (naturalIsZero (naturalEqual (nativePhysicalRepeatAction operation) 2))
230 (naturalNonzero depth))
231 (induction
232 (aosChoose
233 Nat
234 (naturalEqual (nativePhysicalRepeatAction operation) 1)
235 (succ depth)
236 (aosChoose
237 Nat
238 (naturalEqual (nativePhysicalRepeatAction operation) 2)
239 (naturalSaturatingSubtract depth 1)
240 depth))
241 closed))))))))))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.