def eq_refl

bendtorch-core@0.1.0.0 · src/autograd/backward_PROOF.bend:16

import Base

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