def le_case

bend-lawful-stdlib@0.1.0.0 · src/nat.bend:99

import Base

99# Compares a and b and returns the proof of the side that holds.
100def le_case(a: Nat, b: Nat) -> Or(LE(a, b), LE(b, a)):
101  match a b:
102    case 0n y:
103      Inl{Unit{}}
104    case 1n+x 0n:
105      Inr{Unit{}}
106    case 1n+x 1n+y:
107      le_case(x, y)