A jump may skip a complete loop, but may neither enter nor leave one.
Checking the isolated prefix also refuses skipping an end and a different
begin, which comparing only the source and target nesting depth would miss.
866def nativePhysicalBranchWindowValid =
867 (lambda unrestricted count : (family ModelWord64) .
868 (lambda unrestricted rest : (family NativePhysicalCommands) .
869 (let unrestricted prefix =
870 (nativePhysicalCommandsTake rest (modelWord64Natural count))
871 in
872 (naturalAnd
873 (naturalEqual (nativePhysicalCommandsLength prefix) (modelWord64Natural count))
874 (naturalEqual (nativePhysicalRepeatBalance prefix) 0)))))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.