~/jendhub

def wsd.l

bend-osdev-word64@0.1.1.0 · PROOF_text.bend:347

import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W

347def wsd.l(+a: W.W64, pr: {Nat.add(Nat.mul(W.W64.to_nat(wsh.q(a)), 10n), U32.to_nat(wsh.r(a))) == W.W64.to_nat(a) : Nat} & {Nat.is_lt(U32.to_nat(wsh.r(a)), 10n) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(wsh.r(a)), 10n) == True{} : Bool}:
348  (+u, +w) = pr
349  w

Uses (12)

Used by (1)