Library zoo_std.int__code

Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo.options.

Definition intΩ min : val :=
  π—³π˜‚𝗻 "n1" "n2" β†’
    π—Άπ—³ "n1" < "n2" π˜π—΅π—²π—» (
      "n1"
    ) π—²π—Ήπ˜€π—² (
      "n2"
    ).

Definition intΩ max : val :=
  π—³π˜‚𝗻 "n1" "n2" β†’
    π—Άπ—³ "n1" < "n2" π˜π—΅π—²π—» (
      "n2"
    ) π—²π—Ήπ˜€π—² (
      "n1"
    ).

Definition intΩ positive_part : val :=
  π—³π˜‚𝗻 "t" β†’
    intΩ max 0 "t".