~/jendhub

def wsd.snd

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

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

183def wsd.snd(-x: Nat, -y: Nat, -c: Nat, -d: Nat, pr: {x == y : Nat} & {Nat.is_lt(c, d) == True{} : Bool}) -> {Nat.is_lt(c, d) == True{} : Bool}:
184  (+u, +v) = pr
185  v

Uses (5)

Used by (1)