{-# 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.Agda.Builtin.Nat 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

-- Agda.Builtin.Nat.Nat
d_Nat_6 :: ()
d_Nat_6 = ()
data T_Nat_6 = C_zero_8 | C_suc_12 Integer
-- Agda.Builtin.Nat._+_
d__'43'__14 :: Integer -> Integer -> Integer
d__'43'__14 = (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) :: Integer -> Integer -> Integer)
-- Agda.Builtin.Nat._-_
d__'45'__22 :: Integer -> Integer -> Integer
d__'45'__22
  = ((\ Integer
x Integer
y -> Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
0 (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)) :: Integer -> Integer -> Integer)
-- Agda.Builtin.Nat._*_
d__'42'__32 :: Integer -> Integer -> Integer
d__'42'__32 = (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*) :: Integer -> Integer -> Integer)
-- Agda.Builtin.Nat._==_
d__'61''61'__40 :: Integer -> Integer -> Bool
d__'61''61'__40 = (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: Integer -> Integer -> Bool)
-- Agda.Builtin.Nat._<_
d__'60'__46 :: Integer -> Integer -> Bool
d__'60'__46 = (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
(<) :: Integer -> Integer -> Bool)
-- Agda.Builtin.Nat.div-helper
d_div'45'helper_60 :: Integer -> Integer -> Integer -> Integer -> Integer
d_div'45'helper_60
  = ((\ Integer
k Integer
m Integer
n Integer
j -> Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
0 (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j) (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)) :: Integer -> Integer -> Integer -> Integer -> Integer)
-- Agda.Builtin.Nat.mod-helper
d_mod'45'helper_90 :: Integer -> Integer -> Integer -> Integer -> Integer
d_mod'45'helper_90
  = ((\ Integer
k Integer
m Integer
n Integer
j -> if Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
j then Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) (Integer
m Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) else (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
n)) :: Integer -> Integer -> Integer -> Integer -> Integer)