def le_refl

bendtorch-core@0.1.0.0 · src/storage/api.bend:145

import bendtorch-core@0.1.0.0/src/storage/api.bend as Api

import Base

145def le_refl(+k: Nat) -> {Nat.is_le(k, k) == True{} : Bool}:
146  match k:
147    case 0n:
148      {==}
149    case 1n+p:
150      le_refl(p)

Uses (3)

Used by (7)