the position + 1 of the op labelled `label` (0 when none is)
2441def sm121LowerFind =
2442 (lambda unrestricted labels : (family SM121LowerLabels) .
2443 (lambda unrestricted label : Nat .
2444 (eliminate
2445 SM121LowerLabels
2446 (lambda unrestricted current : (family SM121LowerLabels) . Nat)
2447 labels
2448 (branch SM121LowerLabelsEnd . zero)
2449 (branch SM121LowerLabelsNext entry position tail induction .
2450 (naturalSelect (naturalEqual entry label) (succ position) induction)))))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.