~/jendhub

def same_refl

bendtorch-core@0.1.0.0 · src/autograd/tensor_vjp_PROOF.bend:898

import bendtorch-core@0.1.0.0/src/autograd/tensor_vjp_PROOF.bend as TensorVjpPROOF
import Base

898def same_refl(+number: Nat) -> {True{} == Nat.is_eq(number, number) : Bool}:
899  match number:
900    case 0n:
901      {==}
902    case 1n+rest:
903      same_refl(rest)

Uses (3)

Used by (1)