def eq_refl

bendtorch-core@0.1.0.0 · src/autograd/tensor_backward_PROOF.bend:18

import Base

18def eq_refl(+number: Nat) -> {True{} == Nat.is_eq(number, number) : Bool}:
19  match number:
20    case 0n:
21      {==}
22    case 1n+rest:
23      eq_refl(rest)