| 123456789101112131415161718192021222324252627282930313233343536 |
- 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 >
|
