def eq_true

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

import Base

41def eq_true(+a: Nat, -b: Nat, equal: {a == b : Nat}) -> {True{} == Nat.is_eq(a, b) : Bool}:
42  %equal : {True{} == Nat.is_eq(a, _) : Bool}
43  is_eq_refl(a)