~/jendhub

def Health.pick

gralha-bendquest@0.1.0.0 · health.bend:173

import gralha-bendquest@0.1.0.0/health.bend as Health
import Base

173# These implementations use Base arithmetic, which the native compiler
174# implements with big integers. The refinement proofs below tie the fast
175# implementations to the inductive specification above.
176def Health.pick(+order: Cmp, +a: Nat, +b: Nat) -> Nat:
177  match order:
178    case LT{}:
179      a
180    case EQ{}:
181      a
182    case GT{}:
183      b

Uses (2)

Used by (2)