{-# 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.Divisibility.Core 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.Equality
import qualified MAlonzo.Code.Data.Nat.Base

-- Data.Nat.Divisibility.Core._∣_
d__'8739'__20 :: p -> p -> ()
d__'8739'__20 p
a0 p
a1 = ()
newtype T__'8739'__20 = C_divides_34 Integer
-- Data.Nat.Divisibility.Core._∣_.quotient
d_quotient_30 :: T__'8739'__20 -> Integer
d_quotient_30 :: T__'8739'__20 -> Integer
d_quotient_30 T__'8739'__20
v0
  = case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v0 of
      C_divides_34 Integer
v1 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
      T__'8739'__20
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.Core._∣_.equality
d_equality_32 ::
  T__'8739'__20 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_equality_32 :: T__'8739'__20 -> T__'8801'__12
d_equality_32 = T__'8739'__20 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.Divisibility.Core._∤_
d__'8740'__36 :: Integer -> Integer -> ()
d__'8740'__36 :: Integer -> Integer -> ()
d__'8740'__36 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Divisibility.Core._HasNonTrivialDivisorLessThan_
d__HasNonTrivialDivisorLessThan__50 :: p -> p -> ()
d__HasNonTrivialDivisorLessThan__50 p
a0 p
a1 = ()
data T__HasNonTrivialDivisorLessThan__50
  = C_hasNonTrivialDivisor_72 Integer
                              MAlonzo.Code.Data.Nat.Base.T__'8804'__22 T__'8739'__20
-- Data.Nat.Divisibility.Core._HasNonTrivialDivisorLessThan_.divisor
d_divisor_64 :: T__HasNonTrivialDivisorLessThan__50 -> Integer
d_divisor_64 :: T__HasNonTrivialDivisorLessThan__50 -> Integer
d_divisor_64 T__HasNonTrivialDivisorLessThan__50
v0
  = case T__HasNonTrivialDivisorLessThan__50
-> T__HasNonTrivialDivisorLessThan__50
forall a b. a -> b
coe T__HasNonTrivialDivisorLessThan__50
v0 of
      C_hasNonTrivialDivisor_72 Integer
v1 T__'8804'__22
v3 T__'8739'__20
v4 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
      T__HasNonTrivialDivisorLessThan__50
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.Core._HasNonTrivialDivisorLessThan_.divisor-<
d_divisor'45''60'_68 ::
  T__HasNonTrivialDivisorLessThan__50 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_divisor'45''60'_68 :: T__HasNonTrivialDivisorLessThan__50 -> T__'8804'__22
d_divisor'45''60'_68 T__HasNonTrivialDivisorLessThan__50
v0
  = case T__HasNonTrivialDivisorLessThan__50
-> T__HasNonTrivialDivisorLessThan__50
forall a b. a -> b
coe T__HasNonTrivialDivisorLessThan__50
v0 of
      C_hasNonTrivialDivisor_72 Integer
v1 T__'8804'__22
v3 T__'8739'__20
v4 -> T__'8804'__22 -> T__'8804'__22
forall a b. a -> b
coe T__'8804'__22
v3
      T__HasNonTrivialDivisorLessThan__50
_ -> T__'8804'__22
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.Core._HasNonTrivialDivisorLessThan_.divisor-∣
d_divisor'45''8739'_70 ::
  T__HasNonTrivialDivisorLessThan__50 -> T__'8739'__20
d_divisor'45''8739'_70 :: T__HasNonTrivialDivisorLessThan__50 -> T__'8739'__20
d_divisor'45''8739'_70 T__HasNonTrivialDivisorLessThan__50
v0
  = case T__HasNonTrivialDivisorLessThan__50
-> T__HasNonTrivialDivisorLessThan__50
forall a b. a -> b
coe T__HasNonTrivialDivisorLessThan__50
v0 of
      C_hasNonTrivialDivisor_72 Integer
v1 T__'8804'__22
v3 T__'8739'__20
v4 -> T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v4
      T__HasNonTrivialDivisorLessThan__50
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.Core.*-pres-∣
d_'42''45'pres'45''8739'_74 ::
  Integer ->
  Integer ->
  Integer ->
  Integer -> T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
d_'42''45'pres'45''8739'_74 :: Integer
-> Integer
-> Integer
-> Integer
-> T__'8739'__20
-> T__'8739'__20
-> T__'8739'__20
d_'42''45'pres'45''8739'_74 ~Integer
v0 ~Integer
v1 ~Integer
v2 ~Integer
v3 T__'8739'__20
v4 T__'8739'__20
v5
  = T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'42''45'pres'45''8739'_74 T__'8739'__20
v4 T__'8739'__20
v5
du_'42''45'pres'45''8739'_74 ::
  T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'42''45'pres'45''8739'_74 :: T__'8739'__20 -> T__'8739'__20 -> T__'8739'__20
du_'42''45'pres'45''8739'_74 T__'8739'__20
v0 T__'8739'__20
v1
  = case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v0 of
      C_divides_34 Integer
v2
        -> case T__'8739'__20 -> T__'8739'__20
forall a b. a -> b
coe T__'8739'__20
v1 of
             C_divides_34 Integer
v4 -> (Integer -> T__'8739'__20) -> Integer -> T__'8739'__20
forall a b. a -> b
coe Integer -> T__'8739'__20
C_divides_34 (Integer -> Integer -> Integer
mulInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe Integer
v4))
             T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8739'__20
_ -> T__'8739'__20
forall a. a
MAlonzo.RTE.mazUnreachableError