~/jendhub

def pick_strict_lower

stelliferous@0.0.2.0 · proofs/nat_extrema.bend:74

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

74def pick_strict_lower(choice: Bool,+left: Nat,+right: Nat,+lower: Nat,left_ok: {Nat.is_lt(lower,left) == True{} : Bool},right_ok: {Nat.is_lt(lower,right) == True{} : Bool}) ->
75  {Nat.is_lt(lower,Bool.pick(Nat,choice,left,right)) == True{} : Bool}:
76  match choice:
77    case False{}: right_ok
78    case True{}: left_ok

Uses (4)

Used by (1)