---- frames of both combines ----
Every identity either combine derives keeps its base anchor's
composition, so the composition names the combine for any transfer --
including transfers between other owners, which admission also checks.
795def dpoIsAssembly =
796 (lambda unrestricted identity : (family RegionTransferIdentity) .
797 (eliminate
798 RegionTransferIdentity
799 (lambda unrestricted current : (family RegionTransferIdentity) . Nat)
800 identity
801 (branch
802 RegionTransferIdentityOf
803 composition
804 run
805 region
806 representation
807 round
808 operation
809 sender
810 receiver
811 interval
812 .
813 (bytes-equal composition dpoAssembleComposition))))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.