def bq.nt
import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as ProofBsearchimport Base
134def bq.nt(n: Nat) -> Type:
135 match n:
136 case 0n:
137 Unit
138 case 1n+p:
139 Empty
import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as ProofBsearchimport Base
134def bq.nt(n: Nat) -> Type:
135 match n:
136 case 0n:
137 Unit
138 case 1n+p:
139 Empty