does the schema carry at least one entry of the category?
498def continuationSchemaHasCategory =
499 (lambda unrestricted category : (family ContinuationCategory) .
500 (lambda unrestricted schema : (family ContinuationSchema) .
501 (eliminate
502 StdList
503 (lambda unrestricted current : (family StdList (family ContinuationEntry)) .
504 (family StdBool))
505 (continuationSchemaEntriesOf schema)
506 (branch StdListEmpty . (constructor StdBool StdFalse))
507 (branch
508 StdListCons
509 head
510 tail
511 induction
512 .
513 (stdBoolOr
514 (stdBoolFromNatural
515 (naturalEqual
516 (continuationCategoryCode (continuationEntryCategoryOf head))
517 (continuationCategoryCode category)))
518 induction)))))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.