def leb_refl

bend-ml-tensor-array@0.1.19.0 · main.bend:1507

import bend-ml-tensor-array@0.1.19.0/main.bend as BendMlTensorArray

import Base

1507# a <= a
1508def leb_refl(+a: Nat) -> {True{} == leb(a, a) : Bool}:
1509  match a:
1510    case 0n:
1511      {==}
1512    case 1n+p:
1513      leb_refl(p)

Uses (3)

Used by (3)