341def capturePolicyAdmission =
342 (lambda unrestricted policy : (family CapturePolicy) .
343 (eliminate
344 CapturePolicy
345 (lambda unrestricted current : (family CapturePolicy) . Nat)
346 policy
347 (branch
348 CapturePolicyValue
349 version
350 identity
351 profile
352 content
353 ordinary
354 reserved
355 bytes
356 dimensions
357 flush
358 required
359 .
360 (naturalAnd
361 (naturalEqual version 1)
362 (naturalAnd
363 (aosIsIdentity identity)
364 (naturalAnd
365 (naturalLessOrEqual content 1)
366 (naturalAnd
367 (naturalLessOrEqual required 1)
368 (naturalAnd
369 (naturalLessOrEqual 2 reserved)
370 (naturalAnd
371 (naturalLessOrEqual (naturalAdd ordinary reserved) 1024)
372 (naturalAnd
373 (naturalNonzero bytes)
374 (naturalAnd
375 (naturalLessOrEqual bytes 18446744073709551615)
376 (naturalAnd
377 (naturalLessOrEqual dimensions 18446744073709551615)
378 (naturalAnd
379 (naturalNonzero flush)
380 (naturalAnd
381 (naturalLessOrEqual flush 18446744073709551615)
382 (aosChoose
383 Nat
384 content
385 (naturalEqual (captureProfileLevel profile) 3)
386 1)))))))))))))))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.