Arena/slot admission belongs to the caller's checked plan. The program owns
its command count and declares no fallback; native encoding still validates
the exact identity width, nonempty program and reachable command contracts.
832def nativePhysicalCommandsTake =
833 (lambda unrestricted commands : (family NativePhysicalCommands) .
834 (eliminate
835 NativePhysicalCommands
836 (lambda unrestricted current : (family NativePhysicalCommands) .
837 (pi unrestricted count : Nat . (family NativePhysicalCommands)))
838 commands
839 (branch
840 NativePhysicalCommandsEnd
841 .
842 (lambda unrestricted count : Nat .
843 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)))
844 (branch
845 NativePhysicalCommandsNext
846 head
847 tail
848 induction
849 .
850 (lambda unrestricted count : Nat .
851 (nat-eliminate
852 (lambda unrestricted remaining : Nat . (family NativePhysicalCommands))
853 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)
854 (lambda unrestricted previous : Nat .
855 (lambda unrestricted ignored : (family NativePhysicalCommands) .
856 (constructor
857 NativePhysicalCommands
858 NativePhysicalCommandsNext
859 head
860 (induction previous))))
861 count)))))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.