def LE.from

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

import Base

542# The rewrite is erased at runtime, so a decided bound costs one comparison
543# instead of a unary walk to 2^20.
544def LE.from(+a: Nat, +b: Nat, decided: {True{} == Nat.is_le(a, b) : Bool}) -> LE(a, b):
545  %LE.decided(a, b, decided) : _
546  Unit{}