{-# 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
d_Nat_6 :: ()
d_Nat_6 = ()
data T_Nat_6 = C_zero_8 | C_suc_12 Integer
d__'43'__14 :: Integer -> Integer -> Integer
d__'43'__14 = (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) :: Integer -> Integer -> Integer)
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)
d__'42'__32 :: Integer -> Integer -> Integer
d__'42'__32 = (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*) :: Integer -> Integer -> Integer)
d__'61''61'__40 :: Integer -> Integer -> Bool
d__'61''61'__40 = (Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: Integer -> Integer -> Bool)
d__'60'__46 :: Integer -> Integer -> Bool
d__'60'__46 = (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
(<) :: Integer -> Integer -> Bool)
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)
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)