From c75f1514baca9c3d04e9a8e8aaffe584c6129dbc Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 22 Feb 2023 05:42:56 +0100 Subject: [PATCH] add BoolExtra --- lib/Quox/BoolExtra.idr | 12 ++++++++++++ lib/quox-lib.ipkg | 1 + 2 files changed, 13 insertions(+) create mode 100644 lib/Quox/BoolExtra.idr diff --git a/lib/Quox/BoolExtra.idr b/lib/Quox/BoolExtra.idr new file mode 100644 index 0000000..c592ea9 --- /dev/null +++ b/lib/Quox/BoolExtra.idr @@ -0,0 +1,12 @@ +module Quox.BoolExtra + +import public Data.Bool + + +infixr 5 <&&> +infixr 4 <||> + +public export +(<&&>), (<||>) : Monad m => m Bool -> m Bool -> m Bool +a <&&> b = if !a then b else pure False +a <||> b = if not !a then b else pure True diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg index 064cee6..d24fae4 100644 --- a/lib/quox-lib.ipkg +++ b/lib/quox-lib.ipkg @@ -9,6 +9,7 @@ depends = base, contrib, elab-util, sop, snocvect modules = Quox.NatExtra, + Quox.BoolExtra, Quox.Decidable, Quox.No, Quox.Pretty,