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.
964def nativePhysicalCommandsTake =
965 (lambda unrestricted commands : (family NativePhysicalCommands) .
966 (eliminate
967 NativePhysicalCommands
968 (lambda unrestricted current : (family NativePhysicalCommands) .
969 (pi unrestricted count : Nat . (family NativePhysicalCommands)))
970 commands
971 (branch
972 NativePhysicalCommandsEnd
973 .
974 (lambda unrestricted count : Nat .
975 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)))
976 (branch
977 NativePhysicalCommandsNext
978 head
979 tail
980 induction
981 .
982 (lambda unrestricted count : Nat .
983 (nat-eliminate
984 (lambda unrestricted remaining : Nat . (family NativePhysicalCommands))
985 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)
986 (lambda unrestricted previous : Nat .
987 (lambda unrestricted ignored : (family NativePhysicalCommands) .
988 (constructor
989 NativePhysicalCommands
990 NativePhysicalCommandsNext
991 head
992 (induction previous))))
993 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.