def eq_refl

bendtorch-core@0.1.0.0 · src/storage/arith.bend:54

import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

import Base

54def eq_refl(+a: Nat) -> {Nat.is_eq(a, a) == True{} : Bool}:
55  match a:
56    case 0n:
57      {==}
58    case 1n+p:
59      eq_refl(p)

Uses (3)

Used by (9)