def u.cmp_lt_trans

bend-osdev-u32@0.1.0.0 · PROOF_order.bend:302

import bend-osdev-u32@0.1.0.0/PROOF_order.bend as PROOFOrder

import Base

302def u.cmp_lt_trans(a: U32, b: U32, c: U32, +h1: {U32.cmp(a, b) == LT{} : Cmp}, +h2: {U32.cmp(b, c) == LT{} : Cmp}) -> {U32.cmp(a, c) == LT{} : Cmp}:
303  match a b c:
304    case U32{+x} U32{+y} U32{+z}:
305      wd.lt_trans(32n, x, y, z, h1, h2)

Uses (4)

Used by (4)