def le_reflexive

bendtorch-core@0.1.0.0 · src/tensor/word_conversion.bend:98

import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as WordConversion
import Base

98def le_reflexive(+number: Nat) -> {Nat.is_le(number, number) == True{} : Bool}:
99  match number:
100    case 0n:
101      {==}
102    case 1n+p:
103      le_reflexive(p)

Uses (3)

Used by (37)