def bq.le_refl

bend-osdev-algo@0.1.0.0 · proof_bsearch.bend:154

import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as ProofBsearch

import Base

154def bq.le_refl(x: Nat) -> {Nat.is_le(x, x) == True{} : Bool}:
155  match x:
156    case 0n:
157      {==}
158    case 1n+p:
159      bq.le_refl(p)

Uses (3)

Used by (2)