~/jendhub

def bitseq.lt0

bend-osdev-algo@0.1.0.0 · PROOF.bend:642

import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF
import Base

642def bitseq.lt0(+j: Nat, -T: Type, l: {Nat.is_lt(j, 0n) == True{} : Bool}) -> T:
643  Empty.absurd(T, absurd.ft(Equal.trans(Bool, False{}, Nat.is_lt(j, 0n), True{}, Equal.sym(Bool, Nat.is_lt(j, 0n), False{}, nat.lt_zero(j)), l)))

Uses (8)

Used by (1)