{-# 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

-- Data.Nat.Divisibility.Core._∣_
d__'8739'__12 :: p -> p -> ()
d__'8739'__12 p
a0 p
a1 = ()
newtype T__'8739'__12 = C_divides_26 Integer
-- Data.Nat.Divisibility.Core._∣_.quotient
d_quotient_22 :: T__'8739'__12 -> Integer
d_quotient_22 :: T__'8739'__12 -> Integer
d_quotient_22 T__'8739'__12
v0
  = case T__'8739'__12 -> T__'8739'__12
forall a b. a -> b
coe T__'8739'__12
v0 of
      C_divides_26 Integer
v1 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
      T__'8739'__12
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Nat.Divisibility.Core._∣_.equality
d_equality_24 ::
  T__'8739'__12 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_equality_24 :: T__'8739'__12 -> T__'8801'__12
d_equality_24 = T__'8739'__12 -> T__'8801'__12
forall a. a
erased
-- Data.Nat.Divisibility.Core._∤_
d__'8740'__28 :: Integer -> Integer -> ()
d__'8740'__28 :: Integer -> Integer -> ()
d__'8740'__28 = Integer -> Integer -> ()
forall a. a
erased
-- Data.Nat.Divisibility.Core.*-pres-∣
d_'42''45'pres'45''8739'_42 ::
  Integer ->
  Integer ->
  Integer ->
  Integer -> T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12
d_'42''45'pres'45''8739'_42 :: Integer
-> Integer
-> Integer
-> Integer
-> T__'8739'__12
-> T__'8739'__12
-> T__'8739'__12
d_'42''45'pres'45''8739'_42 ~Integer
v0 ~Integer
v1 ~Integer
v2 ~Integer
v3 T__'8739'__12
v4 T__'8739'__12
v5
  = T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12
du_'42''45'pres'45''8739'_42 T__'8739'__12
v4 T__'8739'__12
v5
du_'42''45'pres'45''8739'_42 ::
  T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12
du_'42''45'pres'45''8739'_42 :: T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12
du_'42''45'pres'45''8739'_42 T__'8739'__12
v0 T__'8739'__12
v1
  = case T__'8739'__12 -> T__'8739'__12
forall a b. a -> b
coe T__'8739'__12
v0 of
      C_divides_26 Integer
v2
        -> case T__'8739'__12 -> T__'8739'__12
forall a b. a -> b
coe T__'8739'__12
v1 of
             C_divides_26 Integer
v4 -> (Integer -> T__'8739'__12) -> Integer -> T__'8739'__12
forall a b. a -> b
coe Integer -> T__'8739'__12
C_divides_26 (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'__12
_ -> T__'8739'__12
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8739'__12
_ -> T__'8739'__12
forall a. a
MAlonzo.RTE.mazUnreachableError