~/jendhub

def pick_upper

stelliferous@0.0.2.0 · proofs/nat_extrema.bend:62

import stelliferous@0.0.2.0/proofs/nat_extrema.bend as NatExtrema
import Base

62def pick_upper(choice: Bool,+left: Nat,+right: Nat,+upper: Nat,left_ok: {Nat.is_le(left,upper) == True{} : Bool},right_ok: {Nat.is_le(right,upper) == True{} : Bool}) ->
63  {Nat.is_le(Bool.pick(Nat,choice,left,right),upper) == True{} : Bool}:
64  match choice:
65    case False{}: right_ok
66    case True{}: left_ok

Uses (4)

Used by (1)