~/jendhub

def eq_refl

bendtorch-core@0.1.0.0 · src/autograd/tensor_chain_PROOF.bend:467

import bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend as TensorChainPROOF
import Base

467# Id arithmetic for the entries newer than the output, as in
468# tensor_backward_PROOF.bend, kept here so this file checks on its own.
469def eq_refl(+number: Nat) -> {True{} == Nat.is_eq(number, number) : Bool}:
470  match number:
471    case 0n:
472      {==}
473    case 1n+rest:
474      eq_refl(rest)

Uses (3)

Used by (1)