module Stdlib.Data.Bool.Base;

import Juvix.Builtin.V1.Bool open public;
import Stdlib.Data.Fixity open;

--- Logical negation.
{-# isabelle-function: {name: "\\<not>"} #-}
not : Bool -> Bool
  | true := false
  | false := true;

syntax operator || logical;

--- Logical disjunction. Evaluated lazily. Cannot be partially applied
builtin bool-or
|| : Bool -> Bool -> Bool
  | true _ := true
  | false a := a;

syntax operator && logical;

--- Logical conjunction. Evaluated lazily. Cannot be partially applied.
builtin bool-and
&& : Bool -> Bool -> Bool
  | true a := a
  | false _ := false;

--- Returns the first argument if ;true;, otherwise it returns the second argument. Evaluated lazily. Cannot be partially applied.
builtin bool-if
ite : {A : Type} -> Bool -> A -> A -> A
  | true a _ := a
  | false _ b := b;

--- Logical disjunction.
or (a b : Bool) : Bool := a || b;

--- Logical conjunction.
and (a b : Bool) : Bool := a && b;

builtin assert
assert (x : Bool) : Bool := x;