EXECUTED_PROGRAM

ret > ExitSuccess
out > CompareNat.compare =
out >   λ a b →
out >     let c = a < b in
out >     case c of
out >       Agda.Builtin.Bool.Bool.false →
out >         let d = b < a in
out >         case d of
out >           Agda.Builtin.Bool.Bool.false → CompareNat.Comparison.equal _
out >           Agda.Builtin.Bool.Bool.true →
out >             CompareNat.Comparison.greater (CompareNat._<_.diff (a - b - 1) _)
out >       Agda.Builtin.Bool.Bool.true →
out >         CompareNat.Comparison.less (CompareNat._<_.diff (b - a - 1) _)
out > CompareNat.compare-lots =
out >   λ a b →
out >     let c = a < b in
out >     case c of
out >       Agda.Builtin.Bool.Bool.false →
out >         let d = b < a in
out >         case d of
out >           Agda.Builtin.Bool.Bool.false → "equal-equal"
out >           Agda.Builtin.Bool.Bool.true → "greater-greater"
out >       Agda.Builtin.Bool.Bool.true → "less-less"
out > CompareNat.main =
out >   Common.IO.then
out >     () () _ _ (Common.IO.putStrLn (CompareNat.compare-lots 1500 2000))
out >     (Common.IO.then
out >        () () _ _ (Common.IO.putStrLn (CompareNat.compare-lots 2000 1500))
out >        (Common.IO.putStrLn (CompareNat.compare-lots 2000 2000)))
out > less-less
out > greater-greater
out > equal-equal
out >
