~/jendhub

def pd.len0

bend-osdev-cbc@0.1.0.0 · PROOF_padded.bend:79

import bend-osdev-cbc@0.1.0.0/PROOF_padded.bend as PROOFPadded
import Base

79def pd.len0(+x: Nat) -> {Nat.is_lt(0n, x) == False{} : Bool} -> {x == 0n : Nat}:
80  match x:
81    case 0n:
82      h => {==}
83    case 1n+p:
84      h => pk.absurd({1n+p == 0n : Nat}, Equal.sym(Bool, True{}, False{}, h))

Uses (5)

Used by (1)