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.
998def nativePhysicalBranchWindowValid =
999 (lambda unrestricted count : (family ModelWord64) .
1000 (lambda unrestricted rest : (family NativePhysicalCommands) .
1001 (let unrestricted prefix =
1002 (nativePhysicalCommandsTake rest (modelWord64Natural count))
1003 in
1004 (naturalAnd
1005 (naturalEqual (nativePhysicalCommandsLength prefix) (modelWord64Natural count))
1006 (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.