~/jendhub

def LE.decided

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

import bendtorch-core@0.1.0.0/src/shape/core.bend as Core
import Base

533def LE.decided(+a: Nat, +b: Nat, decided: {True{} == Nat.is_le(a, b) : Bool}) -> {Unit == LE(a, b) : Data}:
534  match a b:
535    case 0n b:
536      {==}
537    case 1n+p 0n:
538      Empty.absurd({Unit == Empty : Data}, clash(decided))
539    case 1n+p 1n+q:
540      LE.decided(p, q, decided)

Uses (8)

Used by (1)