def le_reflexive
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as WordConversionimport 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)
- bendtorch-core@0.1.0.0/src/tensor/word_conversion:word_natural_exact
- bendtorch-core@0.1.0.0/src/tensor/transform_PROOF:add_cursor_le
- bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof:walk_below
- bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF:permuted_at
- bendtorch-core@0.1.0.0/src/tensor/contracts/binary_proofs:allocated_replayed
- …