F64close.itol: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64close.bend as F64close
Lines 79-86 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64close.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64close.bend&start_line=79&end_line=86

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NE
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC

def itol(+a: F.F64, +b: F.F64, +rel: F.F64, +at: F.F64, +bad: Bool) -> {F.ic_tol(a, b, rel, at, bad) == SF.pick(Result<&2, &2, NE.NumError, Bool>, bad, Fail{NE.BadDomain{}}, Done{NEAR(a, b, rel, at)}) : Result<&2, &2, NE.NumError, Bool>}:
  match bad:
    case True{}:
      {==}
    case False{}:
      +e1 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Bool>, t => Done{F.ic_eq(a, b, rel, at, t)}, F.eq(a, b), SF.eq_s(a, b), FC.eq_value(a, b))
      +e2 = Equal.cong(Bool, Result<&2, &2, NE.NumError, Bool>, t => Done{t}, F.ic_eq(a, b, rel, at, SF.eq_s(a, b)), NEAR(a, b, rel, at), ieq(a, b, rel, at, SF.eq_s(a, b)))
      Equal.trans(Result<&2, &2, NE.NumError, Bool>, Done{F.ic_eq(a, b, rel, at, F.eq(a, b))}, Done{F.ic_eq(a, b, rel, at, SF.eq_s(a, b))}, Done{NEAR(a, b, rel, at)}, e1, e2)

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64close.bend&name=NEAR
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64close.bend&name=ieq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend&name=eq_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=eq_s
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=pick
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=ic_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=ic_tol
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/num.bend&name=NumError