~/jendhub

def is_eq_refl

bendtorch-core@0.1.0.0 · src/shape/plan_proofs.bend:34

import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProofs
import Base

34def is_eq_refl(+value: Nat) -> {True{} == Nat.is_eq(value, value) : Bool}:
35  match value:
36    case 0n:
37      {==}
38    case 1n+p:
39      is_eq_refl(p)

Uses (3)

Used by (1)