{-# 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.Builtin.CInteger 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.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Nat
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Builtin.Integer.Base
import qualified MAlonzo.Code.Data.Integer.Base
import qualified MAlonzo.Code.Data.Integer.Properties
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.Maybe.Effectful
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Effect.Applicative
import qualified MAlonzo.Code.Effect.Functor
import qualified MAlonzo.Code.Effect.Monad
import qualified MAlonzo.Code.Level
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Builtin.CInteger._._*>_
d__'42''62'__6 ::
  () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
d__'42''62'__6 :: () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
d__'42''62'__6
  = let v0 :: b
v0 = T_RawMonad_24 -> b
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34 in
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
         (T_RawApplicative_20 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T_RawApplicative_20 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Effect.Applicative.du__'42''62'__52
           ((T_RawMonad_24 -> T_RawApplicative_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawMonad_24 -> T_RawApplicative_20
MAlonzo.Code.Effect.Monad.d_rawApplicative_32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {b}. b
v0)) AgdaAny
v3 AgdaAny
v4)
-- Builtin.CInteger._._<$_
d__'60''36'__8 ::
  () -> () -> AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
d__'60''36'__8 :: () -> () -> AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
d__'60''36'__8
  = let v0 :: b
v0 = T_RawMonad_24 -> b
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34 in
    AgdaAny -> () -> () -> AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe
      (let v1 :: T_RawApplicative_20
v1 = T_RawMonad_24 -> T_RawApplicative_20
MAlonzo.Code.Effect.Monad.d_rawApplicative_32 (AgdaAny -> T_RawMonad_24
forall a b. a -> b
coe AgdaAny
forall {b}. b
v0) in
       (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 ->
            (T_RawFunctor_24 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_RawFunctor_24 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Effect.Functor.du__'60''36'__32
              ((T_RawApplicative_20 -> T_RawFunctor_24) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawApplicative_20 -> T_RawFunctor_24
MAlonzo.Code.Effect.Applicative.d_rawFunctor_30 (T_RawApplicative_20 -> AgdaAny
forall a b. a -> b
coe T_RawApplicative_20
v1)) AgdaAny
v4
              AgdaAny
v5))
-- Builtin.CInteger._._<$>_
d__'60''36''62'__10 ::
  () -> () -> (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
d__'60''36''62'__10 :: () -> () -> (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
d__'60''36''62'__10 ~()
v0 = () -> (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
du__'60''36''62'__10
du__'60''36''62'__10 ::
  () -> (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
du__'60''36''62'__10 :: () -> (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
du__'60''36''62'__10 ()
v0 AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny)
-> (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
MAlonzo.Code.Data.Maybe.Base.du_map_64 AgdaAny -> AgdaAny
v1
-- Builtin.CInteger._._<&>_
d__'60''38''62'__12 ::
  () -> () -> Maybe AgdaAny -> (AgdaAny -> AgdaAny) -> Maybe AgdaAny
d__'60''38''62'__12 :: () -> () -> Maybe AgdaAny -> (AgdaAny -> AgdaAny) -> Maybe AgdaAny
d__'60''38''62'__12
  = let v0 :: b
v0 = T_RawMonad_24 -> b
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34 in
    AgdaAny
-> ()
-> ()
-> Maybe AgdaAny
-> (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
forall a b. a -> b
coe
      (let v1 :: T_RawApplicative_20
v1 = T_RawMonad_24 -> T_RawApplicative_20
MAlonzo.Code.Effect.Monad.d_rawApplicative_32 (AgdaAny -> T_RawMonad_24
forall a b. a -> b
coe AgdaAny
forall {b}. b
v0) in
       (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 ->
            (T_RawFunctor_24 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_RawFunctor_24 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
MAlonzo.Code.Effect.Functor.du__'60''38''62'__38
              ((T_RawApplicative_20 -> T_RawFunctor_24) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawApplicative_20 -> T_RawFunctor_24
MAlonzo.Code.Effect.Applicative.d_rawFunctor_30 (T_RawApplicative_20 -> AgdaAny
forall a b. a -> b
coe T_RawApplicative_20
v1)) AgdaAny
v4
              AgdaAny
v5))
-- Builtin.CInteger._._<*_
d__'60''42'__14 ::
  () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
d__'60''42'__14 :: () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
d__'60''42'__14
  = let v0 :: b
v0 = T_RawMonad_24 -> b
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34 in
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
         (T_RawApplicative_20 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T_RawApplicative_20 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Effect.Applicative.du__'60''42'__46
           ((T_RawMonad_24 -> T_RawApplicative_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawMonad_24 -> T_RawApplicative_20
MAlonzo.Code.Effect.Monad.d_rawApplicative_32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {b}. b
v0)) AgdaAny
v3 AgdaAny
v4)
-- Builtin.CInteger._._<*>_
d__'60''42''62'__16 ::
  () ->
  () -> Maybe (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
d__'60''42''62'__16 :: ()
-> ()
-> Maybe (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
d__'60''42''62'__16 ~()
v0 ~()
v1 = Maybe (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
du__'60''42''62'__16
du__'60''42''62'__16 ::
  Maybe (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
du__'60''42''62'__16 :: Maybe (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
du__'60''42''62'__16
  = ((AgdaAny -> AgdaAny) -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> Maybe (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> AgdaAny -> Maybe AgdaAny -> AgdaAny
MAlonzo.Code.Data.Maybe.Base.du_maybe_32
      (((AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
MAlonzo.Code.Data.Maybe.Base.du_map_64)
      (let v0 :: b
v0 = Maybe AgdaAny -> b
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
forall {b}. b
v0)))
-- Builtin.CInteger._._<=<_
d__'60''61''60'__18 ::
  () ->
  () ->
  () ->
  (AgdaAny -> Maybe AgdaAny) ->
  (AgdaAny -> Maybe AgdaAny) -> AgdaAny -> Maybe AgdaAny
d__'60''61''60'__18 :: ()
-> ()
-> ()
-> (AgdaAny -> Maybe AgdaAny)
-> (AgdaAny -> Maybe AgdaAny)
-> AgdaAny
-> Maybe AgdaAny
d__'60''61''60'__18 ()
v0 ()
v1 ()
v2 AgdaAny -> Maybe AgdaAny
v3 AgdaAny -> Maybe AgdaAny
v4
  = (T_RawMonad_24
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> Maybe AgdaAny)
-> (AgdaAny -> Maybe AgdaAny)
-> AgdaAny
-> Maybe AgdaAny
forall a b. a -> b
coe
      T_RawMonad_24
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Effect.Monad.du__'60''61''60'__88
      (T_RawMonad_24 -> AgdaAny
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34) AgdaAny -> Maybe AgdaAny
v3 AgdaAny -> Maybe AgdaAny
v4
-- Builtin.CInteger._._<⊛_
d__'60''8859'__20 ::
  () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
d__'60''8859'__20 :: () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
d__'60''8859'__20
  = let v0 :: b
v0 = T_RawMonad_24 -> b
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34 in
    (AgdaAny -> AgdaAny -> AgdaAny)
-> () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe
      (\ AgdaAny
v1 AgdaAny
v2 ->
         (T_RawApplicative_20 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T_RawApplicative_20 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Effect.Applicative.du__'60''8859'__72
           ((T_RawMonad_24 -> T_RawApplicative_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawMonad_24 -> T_RawApplicative_20
MAlonzo.Code.Effect.Monad.d_rawApplicative_32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {b}. b
v0)))
-- Builtin.CInteger._._=<<_
d__'61''60''60'__22 ::
  () ->
  () -> (AgdaAny -> Maybe AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
d__'61''60''60'__22 :: ()
-> ()
-> (AgdaAny -> Maybe AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
d__'61''60''60'__22 ()
v0 ()
v1 AgdaAny -> Maybe AgdaAny
v2 Maybe AgdaAny
v3
  = (T_RawMonad_24 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> Maybe AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
forall a b. a -> b
coe
      T_RawMonad_24 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Effect.Monad.du__'61''60''60'__72
      (T_RawMonad_24 -> AgdaAny
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34) AgdaAny -> Maybe AgdaAny
v2 Maybe AgdaAny
v3
-- Builtin.CInteger._._>=>_
d__'62''61''62'__24 ::
  () ->
  () ->
  () ->
  (AgdaAny -> Maybe AgdaAny) ->
  (AgdaAny -> Maybe AgdaAny) -> AgdaAny -> Maybe AgdaAny
d__'62''61''62'__24 :: ()
-> ()
-> ()
-> (AgdaAny -> Maybe AgdaAny)
-> (AgdaAny -> Maybe AgdaAny)
-> AgdaAny
-> Maybe AgdaAny
d__'62''61''62'__24 ()
v0 ()
v1 ()
v2 AgdaAny -> Maybe AgdaAny
v3 AgdaAny -> Maybe AgdaAny
v4 AgdaAny
v5
  = (T_RawMonad_24
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> Maybe AgdaAny)
-> (AgdaAny -> Maybe AgdaAny)
-> AgdaAny
-> Maybe AgdaAny
forall a b. a -> b
coe
      T_RawMonad_24
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Effect.Monad.du__'62''61''62'__80
      (T_RawMonad_24 -> AgdaAny
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34) AgdaAny -> Maybe AgdaAny
v3 AgdaAny -> Maybe AgdaAny
v4 AgdaAny
v5
-- Builtin.CInteger._._>>_
d__'62''62'__26 ::
  () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
d__'62''62'__26 :: () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
d__'62''62'__26 ()
v0 ()
v1
  = (T_RawMonad_24 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe
      T_RawMonad_24 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Effect.Monad.du__'62''62'__70
      (T_RawMonad_24 -> AgdaAny
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34)
-- Builtin.CInteger._._>>=_
d__'62''62''61'__28 ::
  () ->
  () -> Maybe AgdaAny -> (AgdaAny -> Maybe AgdaAny) -> Maybe AgdaAny
d__'62''62''61'__28 :: ()
-> ()
-> Maybe AgdaAny
-> (AgdaAny -> Maybe AgdaAny)
-> Maybe AgdaAny
d__'62''62''61'__28 ~()
v0 = () -> Maybe AgdaAny -> (AgdaAny -> Maybe AgdaAny) -> Maybe AgdaAny
du__'62''62''61'__28
du__'62''62''61'__28 ::
  () -> Maybe AgdaAny -> (AgdaAny -> Maybe AgdaAny) -> Maybe AgdaAny
du__'62''62''61'__28 :: () -> Maybe AgdaAny -> (AgdaAny -> Maybe AgdaAny) -> Maybe AgdaAny
du__'62''62''61'__28 ()
v0 Maybe AgdaAny
v1 AgdaAny -> Maybe AgdaAny
v2
  = (Maybe AgdaAny -> (AgdaAny -> Maybe AgdaAny) -> Maybe AgdaAny)
-> Maybe AgdaAny -> (AgdaAny -> Maybe AgdaAny) -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> (AgdaAny -> Maybe AgdaAny) -> Maybe AgdaAny
MAlonzo.Code.Data.Maybe.Base.du__'62''62''61'__72 Maybe AgdaAny
v1 AgdaAny -> Maybe AgdaAny
v2
-- Builtin.CInteger._._⊗_
d__'8855'__30 ::
  () ->
  () ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d__'8855'__30 :: () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe T_Σ_14
d__'8855'__30
  = let v0 :: b
v0 = T_RawMonad_24 -> b
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34 in
    (AgdaAny -> AgdaAny -> AgdaAny)
-> () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe T_Σ_14
forall a b. a -> b
coe
      (\ AgdaAny
v1 AgdaAny
v2 ->
         (T_RawApplicative_20 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T_RawApplicative_20 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Effect.Applicative.du__'8855'__76
           ((T_RawMonad_24 -> T_RawApplicative_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawMonad_24 -> T_RawApplicative_20
MAlonzo.Code.Effect.Monad.d_rawApplicative_32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {b}. b
v0)))
-- Builtin.CInteger._._⊛_
d__'8859'__32 ::
  () ->
  () -> Maybe (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
d__'8859'__32 :: ()
-> ()
-> Maybe (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
d__'8859'__32
  = let v0 :: b
v0 = T_RawMonad_24 -> b
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34 in
    (AgdaAny -> AgdaAny -> AgdaAny)
-> ()
-> ()
-> Maybe (AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
forall a b. a -> b
coe
      (\ AgdaAny
v1 AgdaAny
v2 ->
         (T_RawApplicative_20 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T_RawApplicative_20 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Effect.Applicative.du__'8859'__70
           ((T_RawMonad_24 -> T_RawApplicative_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawMonad_24 -> T_RawApplicative_20
MAlonzo.Code.Effect.Monad.d_rawApplicative_32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {b}. b
v0)))
-- Builtin.CInteger._._⊛>_
d__'8859''62'__34 ::
  () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
d__'8859''62'__34 :: () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
d__'8859''62'__34
  = let v0 :: b
v0 = T_RawMonad_24 -> b
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34 in
    (AgdaAny -> AgdaAny -> AgdaAny)
-> () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe
      (\ AgdaAny
v1 AgdaAny
v2 ->
         (T_RawApplicative_20 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T_RawApplicative_20 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Effect.Applicative.du__'8859''62'__74
           ((T_RawMonad_24 -> T_RawApplicative_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawMonad_24 -> T_RawApplicative_20
MAlonzo.Code.Effect.Monad.d_rawApplicative_32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {b}. b
v0)))
-- Builtin.CInteger._.Kleisli
d_Kleisli_36 :: () -> () -> ()
d_Kleisli_36 :: () -> () -> ()
d_Kleisli_36 = () -> () -> ()
forall {b}. b
erased
-- Builtin.CInteger._.ignore
d_ignore_38 ::
  () -> Maybe AgdaAny -> Maybe MAlonzo.Code.Level.T_Lift_8
d_ignore_38 :: () -> Maybe AgdaAny -> Maybe T_Lift_8
d_ignore_38
  = let v0 :: b
v0 = T_RawMonad_24 -> b
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34 in
    AgdaAny -> () -> Maybe AgdaAny -> Maybe T_Lift_8
forall a b. a -> b
coe
      (let v1 :: T_RawApplicative_20
v1 = T_RawMonad_24 -> T_RawApplicative_20
MAlonzo.Code.Effect.Monad.d_rawApplicative_32 (AgdaAny -> T_RawMonad_24
forall a b. a -> b
coe AgdaAny
forall {b}. b
v0) in
       (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 ->
            (T_RawFunctor_24 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_RawFunctor_24 -> AgdaAny -> AgdaAny
MAlonzo.Code.Effect.Functor.du_ignore_40
              ((T_RawApplicative_20 -> T_RawFunctor_24) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawApplicative_20 -> T_RawFunctor_24
MAlonzo.Code.Effect.Applicative.d_rawFunctor_30 (T_RawApplicative_20 -> AgdaAny
forall a b. a -> b
coe T_RawApplicative_20
v1))))
-- Builtin.CInteger._.pure
d_pure_40 :: () -> AgdaAny -> Maybe AgdaAny
d_pure_40 :: () -> AgdaAny -> Maybe AgdaAny
d_pure_40 ~()
v0 = AgdaAny -> Maybe AgdaAny
du_pure_40
du_pure_40 :: AgdaAny -> Maybe AgdaAny
du_pure_40 :: AgdaAny -> Maybe AgdaAny
du_pure_40 = (AgdaAny -> Maybe AgdaAny) -> AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
-- Builtin.CInteger._.rawApplicative
d_rawApplicative_42 ::
  MAlonzo.Code.Effect.Applicative.T_RawApplicative_20
d_rawApplicative_42 :: T_RawApplicative_20
d_rawApplicative_42
  = T_RawApplicative_20 -> T_RawApplicative_20
forall a b. a -> b
coe T_RawApplicative_20
MAlonzo.Code.Data.Maybe.Effectful.du_applicative_24
-- Builtin.CInteger._.rawFunctor
d_rawFunctor_44 :: MAlonzo.Code.Effect.Functor.T_RawFunctor_24
d_rawFunctor_44 :: T_RawFunctor_24
d_rawFunctor_44
  = T_RawFunctor_24 -> T_RawFunctor_24
forall a b. a -> b
coe T_RawFunctor_24
MAlonzo.Code.Data.Maybe.Effectful.du_functor_22
-- Builtin.CInteger._.return
d_return_46 :: () -> AgdaAny -> Maybe AgdaAny
d_return_46 :: () -> AgdaAny -> Maybe AgdaAny
d_return_46
  = let v0 :: b
v0 = T_RawMonad_24 -> b
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34 in
    (AgdaAny -> AgdaAny) -> () -> AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe
      (\ AgdaAny
v1 ->
         (T_RawApplicative_20 -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T_RawApplicative_20 -> AgdaAny -> AgdaAny
MAlonzo.Code.Effect.Applicative.du_return_68
           ((T_RawMonad_24 -> T_RawApplicative_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawMonad_24 -> T_RawApplicative_20
MAlonzo.Code.Effect.Monad.d_rawApplicative_32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {b}. b
v0)))
-- Builtin.CInteger._.unless
d_unless_48 ::
  Bool ->
  Maybe MAlonzo.Code.Level.T_Lift_8 ->
  Maybe MAlonzo.Code.Level.T_Lift_8
d_unless_48 :: Bool -> Maybe T_Lift_8 -> Maybe T_Lift_8
d_unless_48
  = (T_RawMonad_24 -> Bool -> AgdaAny -> AgdaAny)
-> AgdaAny -> Bool -> Maybe T_Lift_8 -> Maybe T_Lift_8
forall a b. a -> b
coe
      T_RawMonad_24 -> Bool -> AgdaAny -> AgdaAny
MAlonzo.Code.Effect.Monad.du_unless_96
      (T_RawMonad_24 -> AgdaAny
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34)
-- Builtin.CInteger._.when
d_when_50 ::
  Bool ->
  Maybe MAlonzo.Code.Level.T_Lift_8 ->
  Maybe MAlonzo.Code.Level.T_Lift_8
d_when_50 :: Bool -> Maybe T_Lift_8 -> Maybe T_Lift_8
d_when_50
  = (T_RawMonad_24 -> Bool -> AgdaAny -> AgdaAny)
-> AgdaAny -> Bool -> Maybe T_Lift_8 -> Maybe T_Lift_8
forall a b. a -> b
coe
      T_RawMonad_24 -> Bool -> AgdaAny -> AgdaAny
MAlonzo.Code.Effect.Monad.du_when_90
      (T_RawMonad_24 -> AgdaAny
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34)
-- Builtin.CInteger._.zip
d_zip_52 ::
  () ->
  () ->
  Maybe AgdaAny ->
  Maybe AgdaAny -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_zip_52 :: () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe T_Σ_14
d_zip_52
  = let v0 :: b
v0 = T_RawMonad_24 -> b
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34 in
    (AgdaAny -> AgdaAny -> AgdaAny)
-> () -> () -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe T_Σ_14
forall a b. a -> b
coe
      (\ AgdaAny
v1 AgdaAny
v2 ->
         (T_RawApplicative_20 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T_RawApplicative_20 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Effect.Applicative.du_zip_66
           ((T_RawMonad_24 -> T_RawApplicative_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawMonad_24 -> T_RawApplicative_20
MAlonzo.Code.Effect.Monad.d_rawApplicative_32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {b}. b
v0)))
-- Builtin.CInteger._.zipWith
d_zipWith_54 ::
  () ->
  () ->
  () ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
d_zipWith_54 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
d_zipWith_54
  = let v0 :: b
v0 = T_RawMonad_24 -> b
forall a b. a -> b
coe T_RawMonad_24
MAlonzo.Code.Data.Maybe.Effectful.du_monad_34 in
    (AgdaAny
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> Maybe AgdaAny
-> Maybe AgdaAny
forall a b. a -> b
coe
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ->
         (T_RawApplicative_20
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T_RawApplicative_20
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Effect.Applicative.du_zipWith_58
           ((T_RawMonad_24 -> T_RawApplicative_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_RawMonad_24 -> T_RawApplicative_20
MAlonzo.Code.Effect.Monad.d_rawApplicative_32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {b}. b
v0)) AgdaAny
v4 AgdaAny
v5
           AgdaAny
v6)
-- Builtin.CInteger.minBound
d_minBound_56 :: Integer
d_minBound_56 :: Integer
d_minBound_56
  = (Integer -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe
      Integer -> Integer
MAlonzo.Code.Data.Integer.Base.d_'45'__260
      ((Integer -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Integer -> Integer -> Integer
MAlonzo.Code.Data.Integer.Base.d__'94'__322 (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
2 :: Integer))
         ((Integer -> Integer -> Integer) -> Integer -> Integer -> AgdaAny
forall a b. a -> b
coe
            Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
            (Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'94'__276
               (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe (Integer
18 :: Integer)))
            (Integer
1 :: Integer)))
-- Builtin.CInteger.maxBound
d_maxBound_58 :: Integer
d_maxBound_58 :: Integer
d_maxBound_58
  = (Integer -> Integer -> Integer) -> AgdaAny -> AgdaAny -> Integer
forall a b. a -> b
coe
      Integer -> Integer -> Integer
MAlonzo.Code.Data.Integer.Base.d__'45'__302
      ((Integer -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Integer -> Integer -> Integer
MAlonzo.Code.Data.Integer.Base.d__'94'__322 (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
2 :: Integer))
         ((Integer -> Integer -> Integer) -> Integer -> Integer -> AgdaAny
forall a b. a -> b
coe
            Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
            (Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'94'__276
               (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe (Integer
18 :: Integer)))
            (Integer
1 :: Integer)))
      (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer))
-- Builtin.CInteger.CInteger
d_CInteger_60 :: ()
d_CInteger_60 = ()
data T_CInteger_60
  = C_cInt_64 Integer MAlonzo.Code.Data.Integer.Base.T__'8804'__26
              MAlonzo.Code.Data.Integer.Base.T__'8804'__26
-- Builtin.CInteger.add
d_add_66 :: T_CInteger_60 -> T_CInteger_60 -> Integer
d_add_66 :: T_CInteger_60 -> T_CInteger_60 -> Integer
d_add_66 T_CInteger_60
v0 T_CInteger_60
v1
  = case T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v0 of
      C_cInt_64 Integer
v2 T__'8804'__26
v3 T__'8804'__26
v4
        -> case T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v1 of
             C_cInt_64 Integer
v5 T__'8804'__26
v6 T__'8804'__26
v7
               -> (Integer -> Integer -> Integer) -> AgdaAny -> AgdaAny -> Integer
forall a b. a -> b
coe
                    Integer -> Integer -> Integer
MAlonzo.Code.Data.Integer.Base.d__'43'__284 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5)
             T_CInteger_60
_ -> Integer
forall {b}. b
MAlonzo.RTE.mazUnreachableError
      T_CInteger_60
_ -> Integer
forall {b}. b
MAlonzo.RTE.mazUnreachableError
-- Builtin.CInteger.subtract
d_subtract_72 :: T_CInteger_60 -> T_CInteger_60 -> Integer
d_subtract_72 :: T_CInteger_60 -> T_CInteger_60 -> Integer
d_subtract_72 T_CInteger_60
v0 T_CInteger_60
v1
  = case T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v0 of
      C_cInt_64 Integer
v2 T__'8804'__26
v3 T__'8804'__26
v4
        -> case T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v1 of
             C_cInt_64 Integer
v5 T__'8804'__26
v6 T__'8804'__26
v7
               -> (Integer -> Integer -> Integer) -> AgdaAny -> AgdaAny -> Integer
forall a b. a -> b
coe
                    Integer -> Integer -> Integer
MAlonzo.Code.Data.Integer.Base.d__'45'__302 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5)
             T_CInteger_60
_ -> Integer
forall {b}. b
MAlonzo.RTE.mazUnreachableError
      T_CInteger_60
_ -> Integer
forall {b}. b
MAlonzo.RTE.mazUnreachableError
-- Builtin.CInteger.multiply
d_multiply_78 :: T_CInteger_60 -> T_CInteger_60 -> Integer
d_multiply_78 :: T_CInteger_60 -> T_CInteger_60 -> Integer
d_multiply_78 T_CInteger_60
v0 T_CInteger_60
v1
  = case T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v0 of
      C_cInt_64 Integer
v2 T__'8804'__26
v3 T__'8804'__26
v4
        -> case T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v1 of
             C_cInt_64 Integer
v5 T__'8804'__26
v6 T__'8804'__26
v7
               -> (Integer -> Integer -> Integer) -> AgdaAny -> AgdaAny -> Integer
forall a b. a -> b
coe
                    Integer -> Integer -> Integer
MAlonzo.Code.Data.Integer.Base.d__'42'__316 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5)
             T_CInteger_60
_ -> Integer
forall {b}. b
MAlonzo.RTE.mazUnreachableError
      T_CInteger_60
_ -> Integer
forall {b}. b
MAlonzo.RTE.mazUnreachableError
-- Builtin.CInteger.quot
d_quot_84 :: T_CInteger_60 -> T_CInteger_60 -> Maybe Integer
d_quot_84 :: T_CInteger_60 -> T_CInteger_60 -> Maybe Integer
d_quot_84 T_CInteger_60
v0 T_CInteger_60
v1
  = case T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v0 of
      C_cInt_64 Integer
v2 T__'8804'__26
v3 T__'8804'__26
v4
        -> case T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v1 of
             C_cInt_64 Integer
v5 T__'8804'__26
v6 T__'8804'__26
v7
               -> (Integer -> Integer -> Maybe Integer)
-> AgdaAny -> AgdaAny -> Maybe Integer
forall a b. a -> b
coe
                    Integer -> Integer -> Maybe Integer
MAlonzo.Code.Builtin.Integer.Base.d_quotMaybe_94 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5)
             T_CInteger_60
_ -> Maybe Integer
forall {b}. b
MAlonzo.RTE.mazUnreachableError
      T_CInteger_60
_ -> Maybe Integer
forall {b}. b
MAlonzo.RTE.mazUnreachableError
-- Builtin.CInteger.rem
d_rem_90 :: T_CInteger_60 -> T_CInteger_60 -> Maybe Integer
d_rem_90 :: T_CInteger_60 -> T_CInteger_60 -> Maybe Integer
d_rem_90 T_CInteger_60
v0 T_CInteger_60
v1
  = case T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v0 of
      C_cInt_64 Integer
v2 T__'8804'__26
v3 T__'8804'__26
v4
        -> case T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v1 of
             C_cInt_64 Integer
v5 T__'8804'__26
v6 T__'8804'__26
v7
               -> (Integer -> Integer -> Maybe Integer)
-> AgdaAny -> AgdaAny -> Maybe Integer
forall a b. a -> b
coe
                    Integer -> Integer -> Maybe Integer
MAlonzo.Code.Builtin.Integer.Base.d_remMaybe_120 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5)
             T_CInteger_60
_ -> Maybe Integer
forall {b}. b
MAlonzo.RTE.mazUnreachableError
      T_CInteger_60
_ -> Maybe Integer
forall {b}. b
MAlonzo.RTE.mazUnreachableError
-- Builtin.CInteger.divMod
d_divMod_96 ::
  T_CInteger_60 ->
  T_CInteger_60 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_divMod_96 :: T_CInteger_60 -> T_CInteger_60 -> Maybe T_Σ_14
d_divMod_96 T_CInteger_60
v0 T_CInteger_60
v1
  = case T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v0 of
      C_cInt_64 Integer
v2 T__'8804'__26
v3 T__'8804'__26
v4
        -> case T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v1 of
             C_cInt_64 Integer
v5 T__'8804'__26
v6 T__'8804'__26
v7
               -> (Integer -> Integer -> Maybe T_Σ_14)
-> AgdaAny -> AgdaAny -> Maybe T_Σ_14
forall a b. a -> b
coe
                    Integer -> Integer -> Maybe T_Σ_14
MAlonzo.Code.Builtin.Integer.Base.d_divModMaybe_146 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
                    (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5)
             T_CInteger_60
_ -> Maybe T_Σ_14
forall {b}. b
MAlonzo.RTE.mazUnreachableError
      T_CInteger_60
_ -> Maybe T_Σ_14
forall {b}. b
MAlonzo.RTE.mazUnreachableError
-- Builtin.CInteger.div
d_div_102 :: T_CInteger_60 -> T_CInteger_60 -> Maybe Integer
d_div_102 :: T_CInteger_60 -> T_CInteger_60 -> Maybe Integer
d_div_102 T_CInteger_60
v0 T_CInteger_60
v1
  = ((AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny)
-> (AgdaAny -> AgdaAny) -> Maybe T_Σ_14 -> Maybe Integer
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
MAlonzo.Code.Data.Maybe.Base.du_map_64
      (\ AgdaAny
v2 -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v2))
      (T_CInteger_60 -> T_CInteger_60 -> Maybe T_Σ_14
d_divMod_96 (T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v0) (T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v1))
-- Builtin.CInteger.mod
d_mod_108 :: T_CInteger_60 -> T_CInteger_60 -> Maybe Integer
d_mod_108 :: T_CInteger_60 -> T_CInteger_60 -> Maybe Integer
d_mod_108 T_CInteger_60
v0 T_CInteger_60
v1
  = ((AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny)
-> (AgdaAny -> AgdaAny) -> Maybe T_Σ_14 -> Maybe Integer
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
MAlonzo.Code.Data.Maybe.Base.du_map_64
      (\ AgdaAny
v2 -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v2))
      (T_CInteger_60 -> T_CInteger_60 -> Maybe T_Σ_14
d_divMod_96 (T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v0) (T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v1))
-- Builtin.CInteger.lessThan
d_lessThan_114 :: T_CInteger_60 -> T_CInteger_60 -> Bool
d_lessThan_114 :: T_CInteger_60 -> T_CInteger_60 -> Bool
d_lessThan_114 T_CInteger_60
v0 T_CInteger_60
v1
  = case T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v0 of
      C_cInt_64 Integer
v2 T__'8804'__26
v3 T__'8804'__26
v4
        -> case T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v1 of
             C_cInt_64 Integer
v5 T__'8804'__26
v6 T__'8804'__26
v7
               -> (T_Dec_20 -> Bool) -> AgdaAny -> Bool
forall a b. a -> b
coe
                    T_Dec_20 -> Bool
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_isYes_132
                    ((Integer -> Integer -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Integer.Properties.d__'60''63'__3190 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
                       (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5))
             T_CInteger_60
_ -> Bool
forall {b}. b
MAlonzo.RTE.mazUnreachableError
      T_CInteger_60
_ -> Bool
forall {b}. b
MAlonzo.RTE.mazUnreachableError
-- Builtin.CInteger.lessThanEquals
d_lessThanEquals_120 :: T_CInteger_60 -> T_CInteger_60 -> Bool
d_lessThanEquals_120 :: T_CInteger_60 -> T_CInteger_60 -> Bool
d_lessThanEquals_120 T_CInteger_60
v0 T_CInteger_60
v1
  = case T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v0 of
      C_cInt_64 Integer
v2 T__'8804'__26
v3 T__'8804'__26
v4
        -> case T_CInteger_60 -> T_CInteger_60
forall a b. a -> b
coe T_CInteger_60
v1 of
             C_cInt_64 Integer
v5 T__'8804'__26
v6 T__'8804'__26
v7
               -> (T_Dec_20 -> Bool) -> AgdaAny -> Bool
forall a b. a -> b
coe
                    T_Dec_20 -> Bool
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_isYes_132
                    ((Integer -> Integer -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Integer.Properties.d__'8804''63'__2880 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
                       (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5))
             T_CInteger_60
_ -> Bool
forall {b}. b
MAlonzo.RTE.mazUnreachableError
      T_CInteger_60
_ -> Bool
forall {b}. b
MAlonzo.RTE.mazUnreachableError