def is_eq_refl

bend-collections-laws-math@1.0.0.0 · proofs/lib/nat.bend:234

import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as Nat

import Base

234def is_eq_refl(+a: Nat) -> {Nat.is_eq(a, a) == True{} : Bool}:
235  match a:
236    case 0n:
237      {==}
238    case 1n+p:
239      is_eq_refl(p)

Uses (3)

Used by (12)