{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Data.Nat.Base where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Nat
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Data.Empty

-- Data.Nat.Base._≤ᵇ_
d__'8804''7495'__10 :: Integer -> Integer -> Bool
d__'8804''7495'__10 :: Integer -> Integer -> Bool
d__'8804''7495'__10 Integer
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> Bool
forall a b. a -> b
coe ((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Bool
ltInt (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
-- Data.Nat.Base._≤_
d__'8804'__18 :: p -> p -> ()
d__'8804'__18 p
a0 p
a1 = ()
data T__'8804'__18 = C_z'8804'n_22 | C_s'8804's_30 T__'8804'__18
-- Data.Nat.Base._<_
d__'60'__32 :: Integer -> Integer -> ()
d__'60'__32 :: Integer -> Integer -> ()
d__'60'__32 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≥_
d__'8805'__38 :: Integer -> Integer -> ()
d__'8805'__38 :: Integer -> Integer -> ()
d__'8805'__38 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._>_
d__'62'__44 :: Integer -> Integer -> ()
d__'62'__44 :: Integer -> Integer -> ()
d__'62'__44 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≰_
d__'8816'__50 :: Integer -> Integer -> ()
d__'8816'__50 :: Integer -> Integer -> ()
d__'8816'__50 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≮_
d__'8814'__56 :: Integer -> Integer -> ()
d__'8814'__56 :: Integer -> Integer -> ()
d__'8814'__56 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≱_
d__'8817'__62 :: Integer -> Integer -> ()
d__'8817'__62 :: Integer -> Integer -> ()
d__'8817'__62 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≯_
d__'8815'__68 :: Integer -> Integer -> ()
d__'8815'__68 :: Integer -> Integer -> ()
d__'8815'__68 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base.NonZero
d_NonZero_74 :: Integer -> ()
d_NonZero_74 :: Integer -> ()
d_NonZero_74 = Integer -> ()
forall a. a
erased
-- Data.Nat.Base.≢-nonZero
d_'8802''45'nonZero_80 ::
  Integer ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  AgdaAny
d_'8802''45'nonZero_80 :: Integer -> (T__'8801'__12 -> T_'8869'_4) -> Any
d_'8802''45'nonZero_80 Integer
v0 T__'8801'__12 -> T_'8869'_4
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> (T__'8801'__12 -> T_'8869'_4) -> Any -> Any
forall a b. a -> b
coe T__'8801'__12 -> T_'8869'_4
v1 Any
forall a. a
erased
      Integer
_ -> () -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8
-- Data.Nat.Base.>-nonZero
d_'62''45'nonZero_90 :: Integer -> T__'8804'__18 -> AgdaAny
d_'62''45'nonZero_90 :: Integer -> T__'8804'__18 -> Any
d_'62''45'nonZero_90 ~Integer
v0 T__'8804'__18
v1 = T__'8804'__18 -> Any
du_'62''45'nonZero_90 T__'8804'__18
v1
du_'62''45'nonZero_90 :: T__'8804'__18 -> AgdaAny
du_'62''45'nonZero_90 :: T__'8804'__18 -> Any
du_'62''45'nonZero_90 T__'8804'__18
v0
  = (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v0) (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
-- Data.Nat.Base.pred
d_pred_94 :: Integer -> Integer
d_pred_94 :: Integer -> Integer
d_pred_94 Integer
v0
  = (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v0 (Integer
1 :: Integer)
-- Data.Nat.Base._+⋎_
d__'43''8910'__98 :: Integer -> Integer -> Integer
d__'43''8910'__98 :: Integer -> Integer -> Integer
d__'43''8910'__98 Integer
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> Integer
forall a b. a -> b
coe
             ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'43''8910'__98 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
-- Data.Nat.Base._⊔_
d__'8852'__106 :: Integer -> Integer -> Integer
d__'8852'__106 :: Integer -> Integer -> Integer
d__'8852'__106 Integer
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> Integer
forall a b. a -> b
coe
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
                Integer
0 -> Integer -> Any
forall a b. a -> b
coe Integer
v0
                Integer
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                     Any -> Any
forall a b. a -> b
coe
                       ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                          ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'8852'__106 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3))))
-- Data.Nat.Base._⊓_
d__'8851'__116 :: Integer -> Integer -> Integer
d__'8851'__116 :: Integer -> Integer -> Integer
d__'8851'__116 Integer
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> Integer
forall a b. a -> b
coe
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
                Integer
0 -> Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)
                Integer
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                     Any -> Any
forall a b. a -> b
coe
                       ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                          ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'8851'__116 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3))))
-- Data.Nat.Base.⌊_/2⌋
d_'8970'_'47'2'8971'_126 :: Integer -> Integer
d_'8970'_'47'2'8971'_126 :: Integer -> Integer
d_'8970'_'47'2'8971'_126 Integer
v0
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      Integer
1 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      Integer
_ -> let v1 :: Integer
v1 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) in
           Any -> Integer
forall a b. a -> b
coe
             ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                ((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
d_'8970'_'47'2'8971'_126 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
-- Data.Nat.Base.⌈_/2⌉
d_'8968'_'47'2'8969'_130 :: Integer -> Integer
d_'8968'_'47'2'8969'_130 :: Integer -> Integer
d_'8968'_'47'2'8969'_130 Integer
v0
  = (Integer -> Integer) -> Any -> Integer
forall a b. a -> b
coe
      Integer -> Integer
d_'8970'_'47'2'8971'_126 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
-- Data.Nat.Base._^_
d__'94'__134 :: Integer -> Integer -> Integer
d__'94'__134 :: Integer -> Integer -> Integer
d__'94'__134 Integer
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> Integer
forall a b. a -> b
coe ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
d__'94'__134 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2)))
-- Data.Nat.Base.∣_-_∣
d_'8739'_'45'_'8739'_142 :: Integer -> Integer -> Integer
d_'8739'_'45'_'8739'_142 :: Integer -> Integer -> Integer
d_'8739'_'45'_'8739'_142 Integer
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> Integer
forall a b. a -> b
coe
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
                Integer
0 -> Integer -> Any
forall a b. a -> b
coe Integer
v0
                Integer
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                     Any -> Any
forall a b. a -> b
coe ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
d_'8739'_'45'_'8739'_142 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3)))
-- Data.Nat.Base._≤′_
d__'8804''8242'__154 :: p -> p -> ()
d__'8804''8242'__154 p
a0 p
a1 = ()
data T__'8804''8242'__154
  = C_'8804''8242''45'refl_158 |
    C_'8804''8242''45'step_164 T__'8804''8242'__154
-- Data.Nat.Base._<′_
d__'60''8242'__166 :: Integer -> Integer -> ()
d__'60''8242'__166 :: Integer -> Integer -> ()
d__'60''8242'__166 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≥′_
d__'8805''8242'__172 :: Integer -> Integer -> ()
d__'8805''8242'__172 :: Integer -> Integer -> ()
d__'8805''8242'__172 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._>′_
d__'62''8242'__178 :: Integer -> Integer -> ()
d__'62''8242'__178 :: Integer -> Integer -> ()
d__'62''8242'__178 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≤″_
d__'8804''8243'__188 :: p -> p -> ()
d__'8804''8243'__188 p
a0 p
a1 = ()
newtype T__'8804''8243'__188
  = C_less'45'than'45'or'45'equal_202 Integer
-- Data.Nat.Base._≤″_.k
d_k_198 :: T__'8804''8243'__188 -> Integer
d_k_198 :: T__'8804''8243'__188 -> Integer
d_k_198 T__'8804''8243'__188
v0
  = case T__'8804''8243'__188 -> T__'8804''8243'__188
forall a b. a -> b
coe T__'8804''8243'__188
v0 of
      C_less'45'than'45'or'45'equal_202 Integer
v1 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
      T__'8804''8243'__188
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Base._≤″_.proof
d_proof_200 ::
  T__'8804''8243'__188 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_proof_200 :: T__'8804''8243'__188 -> T__'8801'__12
d_proof_200 = T__'8804''8243'__188 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.Base._<″_
d__'60''8243'__204 :: Integer -> Integer -> ()
d__'60''8243'__204 :: Integer -> Integer -> ()
d__'60''8243'__204 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≥″_
d__'8805''8243'__210 :: Integer -> Integer -> ()
d__'8805''8243'__210 :: Integer -> Integer -> ()
d__'8805''8243'__210 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._>″_
d__'62''8243'__216 :: Integer -> Integer -> ()
d__'62''8243'__216 :: Integer -> Integer -> ()
d__'62''8243'__216 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≤‴_
d__'8804''8244'__222 :: p -> p -> ()
d__'8804''8244'__222 p
a0 p
a1 = ()
data T__'8804''8244'__222
  = C_'8804''8244''45'refl_226 |
    C_'8804''8244''45'step_232 T__'8804''8244'__222
-- Data.Nat.Base._<‴_
d__'60''8244'__234 :: Integer -> Integer -> ()
d__'60''8244'__234 :: Integer -> Integer -> ()
d__'60''8244'__234 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._≥‴_
d__'8805''8244'__240 :: Integer -> Integer -> ()
d__'8805''8244'__240 :: Integer -> Integer -> ()
d__'8805''8244'__240 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base._>‴_
d__'62''8244'__246 :: Integer -> Integer -> ()
d__'62''8244'__246 :: Integer -> Integer -> ()
d__'62''8244'__246 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Base.Ordering
d_Ordering_252 :: p -> p -> ()
d_Ordering_252 p
a0 p
a1 = ()
data T_Ordering_252
  = C_less_258 Integer | C_equal_262 | C_greater_268 Integer
-- Data.Nat.Base.compare
d_compare_274 :: Integer -> Integer -> T_Ordering_252
d_compare_274 :: Integer -> Integer -> T_Ordering_252
d_compare_274 Integer
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
             Integer
0 -> T_Ordering_252 -> T_Ordering_252
forall a b. a -> b
coe T_Ordering_252
C_equal_262
             Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                  Any -> T_Ordering_252
forall a b. a -> b
coe ((Integer -> T_Ordering_252) -> Integer -> Any
forall a b. a -> b
coe Integer -> T_Ordering_252
C_less_258 Integer
v2)
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T_Ordering_252
forall a b. a -> b
coe
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
                Integer
0 -> (Integer -> T_Ordering_252) -> Integer -> Any
forall a b. a -> b
coe Integer -> T_Ordering_252
C_greater_268 Integer
v2
                Integer
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                     Any -> Any
forall a b. a -> b
coe ((Integer -> Integer -> T_Ordering_252) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> T_Ordering_252
d_compare_274 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3)))