def le_trans

bendtorch-core@0.1.0.0 · src/tensor/word_conversion.bend:121

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

121def le_trans(+left: Nat, +middle: Nat, +right: Nat,
122  first: {Nat.is_le(left, middle) == True{} : Bool},
123  second: {Nat.is_le(middle, right) == True{} : Bool}) ->
124  {Nat.is_le(left, right) == True{} : Bool}:
125  match left:
126    case 0n:
127      Arith.le_zero(right)
128    case 1n+l:
129      match middle:
130        case 0n:
131          Empty.absurd({Nat.is_le(1n+l, right) == True{} : Bool}, Arith.clash(first))
132        case 1n+m:
133          match right:
134            case 0n:
135              Empty.absurd({Nat.is_le(1n+l, 0n) == True{} : Bool}, Arith.clash(second))
136            case 1n+r:
137              le_trans(l, m, r, first, second)