diff --git a/lib/Quox/BoolExtra.idr b/lib/Quox/BoolExtra.idr index c592ea9..69a7495 100644 --- a/lib/Quox/BoolExtra.idr +++ b/lib/Quox/BoolExtra.idr @@ -3,10 +3,10 @@ module Quox.BoolExtra import public Data.Bool -infixr 5 <&&> -infixr 4 <||> +infixr 5 `andM` +infixr 4 `orM` 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 +andM, orM : Monad m => m Bool -> m Bool -> m Bool +andM a b = if !a then b else pure False +orM a b = if not !a then b else pure True diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index 1e2a61b..f3e815f 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -92,7 +92,7 @@ parameters (defs : Definitions' q g) TYPE _ => pure False Pi {res, _} => isSubSing res.term Lam {} => pure False - Sig {fst, snd} => isSubSing fst <&&> isSubSing snd.term + Sig {fst, snd} => isSubSing fst `andM` isSubSing snd.term Pair {} => pure False Enum tags => pure $ length (SortedSet.toList tags) <= 1 Tag {} => pure False