EXECUTED_PROGRAM

ret > ExitSuccess
out > CaseOnCase.isLess =
out >   λ a →
out >     case a of
out >       CaseOnCase.Cmp.less → Agda.Builtin.Bool.Bool.true
out >       CaseOnCase.Cmp.equal → Agda.Builtin.Bool.Bool.false
out >       CaseOnCase.Cmp.greater → Agda.Builtin.Bool.Bool.false
out > CaseOnCase.compareInt =
out >   λ a b →
out >     let c = CaseOnCase._-_ a b in
out >     case c of
out >       0 → CaseOnCase.Cmp.equal
out >       _ | c >= 1 → CaseOnCase.Cmp.greater
out >       _ → CaseOnCase.Cmp.less
out > CaseOnCase._<_ =
out >   λ a b →
out >     let c = CaseOnCase._-_ a b in
out >     case c of
out >       0 → Agda.Builtin.Bool.Bool.false
out >       _ | c >= 1 → Agda.Builtin.Bool.Bool.false
out >       _ → Agda.Builtin.Bool.Bool.true
out > CaseOnCase.cmp =
out >   λ a b →
out >     let c = CaseOnCase._-_ a b in
out >     case c of
out >       0 → "not less"
out >       _ | c >= 1 → "not less"
out >       _ → "less"
out > CaseOnCase.fancyCase =
out >   λ a b →
out >     case a of
out >       0 → 0
out >       1 → 1
out >       2 → 2
out >       _ → let c = a - 3 in
out >           case b of
out >             CaseOnCase.Cmp.equal → 4
out >             CaseOnCase.Cmp.greater → c
out >             CaseOnCase.Cmp.less → a - 1
out > CaseOnCase.main =
out >   Common.IO.then
out >     () () _ _ (Common.IO.putStrLn (CaseOnCase.cmp 31 -6))
out >     (Common.IO.then
out >        () () _ _ (Common.IO.putStrLn (CaseOnCase.cmp 5 5))
out >        (Common.IO.putStrLn (CaseOnCase.cmp -5 -3)))
out > not less
out > not less
out > less
out >
