def wsd.fst

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

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

import Base

179def wsd.fst(-x: Nat, -y: Nat, -c: Nat, -d: Nat, pr: {x == y : Nat} & {Nat.is_lt(c, d) == True{} : Bool}) -> {x == y : Nat}:
180  (+u, +v) = pr
181  u

Uses (5)

Used by (1)

bend-osdev-word64@0.1.1.0/PROOF_text:wsd.step