{-# 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
d__'8739'__20 :: p -> p -> ()
d__'8739'__20 p
a0 p
a1 = ()
newtype T__'8739'__20 = C_divides_34 Integer
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
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
d__'8740'__36 :: Integer -> Integer -> ()
d__'8740'__36 :: Integer -> Integer -> ()
d__'8740'__36 = Integer -> Integer -> ()
forall a. a
erased
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
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
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
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
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