{-# 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.Utils 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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.List
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

import Raw
import qualified Data.ByteString as BS
import PlutusCore.Data as D
import qualified PlutusCore.Crypto.BLS12_381.G1 as G1
import qualified PlutusCore.Crypto.BLS12_381.G2 as G2
import qualified PlutusCore.Crypto.BLS12_381.Pairing as Pairing
type Pair a b = (a , b)
-- Utils.Either
d_Either_6 :: p -> p -> ()
d_Either_6 p
a0 p
a1 = ()
type T_Either_6 a0 a1 = Either a0 a1
pattern $mC_inj'8321'_12 :: forall {r} {a} {b}. Either a b -> (a -> r) -> ((# #) -> r) -> r
$bC_inj'8321'_12 :: forall {a} {b}. a -> Either a b
C_inj'8321'_12 a0 = Left a0
pattern $mC_inj'8322'_14 :: forall {r} {a} {b}. Either a b -> (b -> r) -> ((# #) -> r) -> r
$bC_inj'8322'_14 :: forall {a} {b}. b -> Either a b
C_inj'8322'_14 a0 = Right a0
check_inj'8321'_12 :: forall xA. forall xB. xA -> T_Either_6 xA xB
check_inj'8321'_12 :: forall {a} {b}. a -> Either a b
check_inj'8321'_12 = xA -> Either xA xB
forall {a} {b}. a -> Either a b
Left
check_inj'8322'_14 :: forall xA. forall xB. xB -> T_Either_6 xA xB
check_inj'8322'_14 :: forall {a} {b}. b -> Either a b
check_inj'8322'_14 = xB -> Either xA xB
forall {a} {b}. b -> Either a b
Right
cover_Either_6 :: Either a1 a2 -> ()
cover_Either_6 :: forall a1 a2. Either a1 a2 -> ()
cover_Either_6 Either a1 a2
x
  = case Either a1 a2
x of
      Left a1
_ -> ()
      Right a2
_ -> ()
-- Utils.either
d_either_22 ::
  () ->
  () ->
  () ->
  T_Either_6 AgdaAny AgdaAny ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny
d_either_22 :: ()
-> ()
-> ()
-> T_Either_6 AgdaAny AgdaAny
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
d_either_22 ~()
v0 ~()
v1 ~()
v2 T_Either_6 AgdaAny AgdaAny
v3 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 = T_Either_6 AgdaAny AgdaAny
-> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny
du_either_22 T_Either_6 AgdaAny AgdaAny
v3 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5
du_either_22 ::
  T_Either_6 AgdaAny AgdaAny ->
  (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny
du_either_22 :: T_Either_6 AgdaAny AgdaAny
-> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny
du_either_22 T_Either_6 AgdaAny AgdaAny
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2
  = case T_Either_6 AgdaAny AgdaAny -> T_Either_6 AgdaAny AgdaAny
forall a b. a -> b
coe T_Either_6 AgdaAny AgdaAny
v0 of
      C_inj'8321'_12 AgdaAny
v3 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3
      C_inj'8322'_14 AgdaAny
v3 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v3
      T_Either_6 AgdaAny AgdaAny
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.eitherBind
d_eitherBind_42 ::
  () ->
  () ->
  () ->
  T_Either_6 AgdaAny AgdaAny ->
  (AgdaAny -> T_Either_6 AgdaAny AgdaAny) ->
  T_Either_6 AgdaAny AgdaAny
d_eitherBind_42 :: ()
-> ()
-> ()
-> T_Either_6 AgdaAny AgdaAny
-> (AgdaAny -> T_Either_6 AgdaAny AgdaAny)
-> T_Either_6 AgdaAny AgdaAny
d_eitherBind_42 ~()
v0 ~()
v1 ~()
v2 T_Either_6 AgdaAny AgdaAny
v3 AgdaAny -> T_Either_6 AgdaAny AgdaAny
v4 = T_Either_6 AgdaAny AgdaAny
-> (AgdaAny -> T_Either_6 AgdaAny AgdaAny)
-> T_Either_6 AgdaAny AgdaAny
du_eitherBind_42 T_Either_6 AgdaAny AgdaAny
v3 AgdaAny -> T_Either_6 AgdaAny AgdaAny
v4
du_eitherBind_42 ::
  T_Either_6 AgdaAny AgdaAny ->
  (AgdaAny -> T_Either_6 AgdaAny AgdaAny) ->
  T_Either_6 AgdaAny AgdaAny
du_eitherBind_42 :: T_Either_6 AgdaAny AgdaAny
-> (AgdaAny -> T_Either_6 AgdaAny AgdaAny)
-> T_Either_6 AgdaAny AgdaAny
du_eitherBind_42 T_Either_6 AgdaAny AgdaAny
v0 AgdaAny -> T_Either_6 AgdaAny AgdaAny
v1
  = case T_Either_6 AgdaAny AgdaAny -> T_Either_6 AgdaAny AgdaAny
forall a b. a -> b
coe T_Either_6 AgdaAny AgdaAny
v0 of
      C_inj'8321'_12 AgdaAny
v2 -> T_Either_6 AgdaAny AgdaAny -> T_Either_6 AgdaAny AgdaAny
forall a b. a -> b
coe T_Either_6 AgdaAny AgdaAny
v0
      C_inj'8322'_14 AgdaAny
v2 -> (AgdaAny -> T_Either_6 AgdaAny AgdaAny)
-> AgdaAny -> T_Either_6 AgdaAny AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Either_6 AgdaAny AgdaAny
v1 AgdaAny
v2
      T_Either_6 AgdaAny AgdaAny
_ -> T_Either_6 AgdaAny AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.decIf
d_decIf_56 ::
  () ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_decIf_56 :: () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny -> AgdaAny
d_decIf_56 ~()
v0 ~()
v1 T_Dec_20
v2 AgdaAny
v3 AgdaAny
v4 = T_Dec_20 -> AgdaAny -> AgdaAny -> AgdaAny
du_decIf_56 T_Dec_20
v2 AgdaAny
v3 AgdaAny
v4
du_decIf_56 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_decIf_56 :: T_Dec_20 -> AgdaAny -> AgdaAny -> AgdaAny
du_decIf_56 T_Dec_20
v0 AgdaAny
v1 AgdaAny
v2
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v3 T_Reflects_16
v4
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v3
             then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
             else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
      T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.cong₃
d_cong'8323'_92 ::
  () ->
  () ->
  () ->
  () ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_cong'8323'_92 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_cong'8323'_92 = ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Utils.≡-subst-removable
d_'8801''45'subst'45'removable_114 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8801''45'subst'45'removable_114 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
d_'8801''45'subst'45'removable_114 = ()
-> ()
-> ()
-> (AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Utils._∔_≣_
d__'8724'_'8803'__120 :: p -> p -> p -> ()
d__'8724'_'8803'__120 p
a0 p
a1 p
a2 = ()
data T__'8724'_'8803'__120
  = C_start_124 | C_bubble_132 T__'8724'_'8803'__120
-- Utils.unique∔
d_unique'8724'_144 ::
  Integer ->
  Integer ->
  Integer ->
  T__'8724'_'8803'__120 ->
  T__'8724'_'8803'__120 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_unique'8724'_144 :: Integer
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> T__'8724'_'8803'__120
-> T__'8801'__12
d_unique'8724'_144 = Integer
-> Integer
-> Integer
-> T__'8724'_'8803'__120
-> T__'8724'_'8803'__120
-> T__'8801'__12
forall a. a
erased
-- Utils.+2∔
d_'43'2'8724'_156 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__'8724'_'8803'__120
d_'43'2'8724'_156 :: Integer
-> Integer -> Integer -> T__'8801'__12 -> T__'8724'_'8803'__120
d_'43'2'8724'_156 Integer
v0 ~Integer
v1 ~Integer
v2 ~T__'8801'__12
v3 = Integer -> T__'8724'_'8803'__120
du_'43'2'8724'_156 Integer
v0
du_'43'2'8724'_156 :: Integer -> T__'8724'_'8803'__120
du_'43'2'8724'_156 :: Integer -> T__'8724'_'8803'__120
du_'43'2'8724'_156 Integer
v0
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T__'8724'_'8803'__120 -> T__'8724'_'8803'__120
forall a b. a -> b
coe T__'8724'_'8803'__120
C_start_124
      Integer
_ -> let v1 :: Integer
v1 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> T__'8724'_'8803'__120
forall a b. a -> b
coe ((T__'8724'_'8803'__120 -> T__'8724'_'8803'__120)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8724'_'8803'__120 -> T__'8724'_'8803'__120
C_bubble_132 ((Integer -> T__'8724'_'8803'__120) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8724'_'8803'__120
du_'43'2'8724'_156 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1)))
-- Utils.∔2+
d_'8724'2'43'_174 ::
  Integer ->
  Integer ->
  Integer ->
  T__'8724'_'8803'__120 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8724'2'43'_174 :: Integer
-> Integer -> Integer -> T__'8724'_'8803'__120 -> T__'8801'__12
d_'8724'2'43'_174 = Integer
-> Integer -> Integer -> T__'8724'_'8803'__120 -> T__'8801'__12
forall a. a
erased
-- Utils.alldone
d_alldone_180 :: Integer -> T__'8724'_'8803'__120
d_alldone_180 :: Integer -> T__'8724'_'8803'__120
d_alldone_180 Integer
v0 = (Integer -> T__'8724'_'8803'__120)
-> AgdaAny -> T__'8724'_'8803'__120
forall a b. a -> b
coe Integer -> T__'8724'_'8803'__120
du_'43'2'8724'_156 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0)
-- Utils.Monad
d_Monad_186 :: p -> ()
d_Monad_186 p
a0 = ()
data T_Monad_186
  = C_Monad'46'constructor_12257 (() -> AgdaAny -> AgdaAny)
                                 (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-- Utils.Monad.return
d_return_202 :: T_Monad_186 -> () -> AgdaAny -> AgdaAny
d_return_202 :: T_Monad_186 -> () -> AgdaAny -> AgdaAny
d_return_202 T_Monad_186
v0
  = case T_Monad_186 -> T_Monad_186
forall a b. a -> b
coe T_Monad_186
v0 of
      C_Monad'46'constructor_12257 () -> AgdaAny -> AgdaAny
v1 () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
v2 -> (() -> AgdaAny -> AgdaAny) -> () -> AgdaAny -> AgdaAny
forall a b. a -> b
coe () -> AgdaAny -> AgdaAny
v1
      T_Monad_186
_ -> () -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.Monad._>>=_
d__'62''62''61'__208 ::
  T_Monad_186 ->
  () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'62''62''61'__208 :: T_Monad_186
-> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'62''62''61'__208 T_Monad_186
v0
  = case T_Monad_186 -> T_Monad_186
forall a b. a -> b
coe T_Monad_186
v0 of
      C_Monad'46'constructor_12257 () -> AgdaAny -> AgdaAny
v1 () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
v2 -> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
v2
      T_Monad_186
_ -> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.Monad._>>_
d__'62''62'__214 ::
  (() -> ()) ->
  T_Monad_186 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d__'62''62'__214 :: (() -> ())
-> T_Monad_186 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d__'62''62'__214 ~() -> ()
v0 T_Monad_186
v1 ~()
v2 ~()
v3 AgdaAny
v4 AgdaAny
v5 = T_Monad_186 -> AgdaAny -> AgdaAny -> AgdaAny
du__'62''62'__214 T_Monad_186
v1 AgdaAny
v4 AgdaAny
v5
du__'62''62'__214 :: T_Monad_186 -> AgdaAny -> AgdaAny -> AgdaAny
du__'62''62'__214 :: T_Monad_186 -> AgdaAny -> AgdaAny -> AgdaAny
du__'62''62'__214 T_Monad_186
v0 AgdaAny
v1 AgdaAny
v2
  = (T_Monad_186
 -> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> T_Monad_186
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe T_Monad_186
-> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'62''62''61'__208 T_Monad_186
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
v1 (\ AgdaAny
v3 -> AgdaAny
v2)
-- Utils.Monad.fmap
d_fmap_224 ::
  (() -> ()) ->
  T_Monad_186 ->
  () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_fmap_224 :: (() -> ())
-> T_Monad_186
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_fmap_224 ~() -> ()
v0 T_Monad_186
v1 ~()
v2 ~()
v3 AgdaAny -> AgdaAny
v4 AgdaAny
v5 = T_Monad_186 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_fmap_224 T_Monad_186
v1 AgdaAny -> AgdaAny
v4 AgdaAny
v5
du_fmap_224 ::
  T_Monad_186 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_fmap_224 :: T_Monad_186 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_fmap_224 T_Monad_186
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_Monad_186
 -> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> T_Monad_186
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
      T_Monad_186
-> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'62''62''61'__208 T_Monad_186
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
v2
      (\ AgdaAny
v3 -> (T_Monad_186 -> () -> AgdaAny -> AgdaAny)
-> T_Monad_186 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monad_186 -> () -> AgdaAny -> AgdaAny
d_return_202 T_Monad_186
v0 AgdaAny
forall a. a
erased ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3))
-- Utils._._>>_
d__'62''62'__232 ::
  (() -> ()) ->
  T_Monad_186 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d__'62''62'__232 :: (() -> ())
-> T_Monad_186 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d__'62''62'__232 ~() -> ()
v0 T_Monad_186
v1 = T_Monad_186 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
du__'62''62'__232 T_Monad_186
v1
du__'62''62'__232 ::
  T_Monad_186 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
du__'62''62'__232 :: T_Monad_186 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
du__'62''62'__232 T_Monad_186
v0 ()
v1 ()
v2 AgdaAny
v3 AgdaAny
v4
  = (T_Monad_186 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monad_186 -> AgdaAny -> AgdaAny -> AgdaAny
du__'62''62'__214 (T_Monad_186 -> AgdaAny
forall a b. a -> b
coe T_Monad_186
v0) AgdaAny
v3 AgdaAny
v4
-- Utils._._>>=_
d__'62''62''61'__234 ::
  T_Monad_186 ->
  () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'62''62''61'__234 :: T_Monad_186
-> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'62''62''61'__234 T_Monad_186
v0 = (T_Monad_186
 -> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> ()
-> ()
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe T_Monad_186
-> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'62''62''61'__208 (T_Monad_186 -> AgdaAny
forall a b. a -> b
coe T_Monad_186
v0)
-- Utils._.fmap
d_fmap_236 ::
  (() -> ()) ->
  T_Monad_186 ->
  () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_fmap_236 :: (() -> ())
-> T_Monad_186
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_fmap_236 ~() -> ()
v0 T_Monad_186
v1 = T_Monad_186
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_fmap_236 T_Monad_186
v1
du_fmap_236 ::
  T_Monad_186 ->
  () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_fmap_236 :: T_Monad_186
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_fmap_236 T_Monad_186
v0 ()
v1 ()
v2 AgdaAny -> AgdaAny
v3 AgdaAny
v4 = (T_Monad_186 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monad_186 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_fmap_224 (T_Monad_186 -> AgdaAny
forall a b. a -> b
coe T_Monad_186
v0) AgdaAny -> AgdaAny
v3 AgdaAny
v4
-- Utils._.return
d_return_238 :: T_Monad_186 -> () -> AgdaAny -> AgdaAny
d_return_238 :: T_Monad_186 -> () -> AgdaAny -> AgdaAny
d_return_238 T_Monad_186
v0 = (T_Monad_186 -> () -> AgdaAny -> AgdaAny)
-> AgdaAny -> () -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monad_186 -> () -> AgdaAny -> AgdaAny
d_return_202 (T_Monad_186 -> AgdaAny
forall a b. a -> b
coe T_Monad_186
v0)
-- Utils.MaybeMonad
d_MaybeMonad_240 :: T_Monad_186
d_MaybeMonad_240 :: T_Monad_186
d_MaybeMonad_240
  = ((() -> AgdaAny -> AgdaAny)
 -> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
 -> T_Monad_186)
-> AgdaAny -> AgdaAny -> T_Monad_186
forall a b. a -> b
coe
      (() -> AgdaAny -> AgdaAny)
-> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> T_Monad_186
C_Monad'46'constructor_12257
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> (AgdaAny -> Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 ->
            (Maybe AgdaAny -> (AgdaAny -> Maybe AgdaAny) -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> (AgdaAny -> Maybe AgdaAny) -> Maybe AgdaAny
MAlonzo.Code.Data.Maybe.Base.du__'62''62''61'__72 AgdaAny
v2 AgdaAny
v3))
-- Utils.sumBind
d_sumBind_248 ::
  () ->
  () ->
  () ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  (AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_sumBind_248 :: ()
-> ()
-> ()
-> T__'8846'__30
-> (AgdaAny -> T__'8846'__30)
-> T__'8846'__30
d_sumBind_248 ~()
v0 ~()
v1 ~()
v2 T__'8846'__30
v3 AgdaAny -> T__'8846'__30
v4 = T__'8846'__30 -> (AgdaAny -> T__'8846'__30) -> T__'8846'__30
du_sumBind_248 T__'8846'__30
v3 AgdaAny -> T__'8846'__30
v4
du_sumBind_248 ::
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  (AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_sumBind_248 :: T__'8846'__30 -> (AgdaAny -> T__'8846'__30) -> T__'8846'__30
du_sumBind_248 T__'8846'__30
v0 AgdaAny -> T__'8846'__30
v1
  = case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v0 of
      MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v2 -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
v1 AgdaAny
v2
      MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v2 -> T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v0
      T__'8846'__30
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.SumMonad
d_SumMonad_262 :: () -> T_Monad_186
d_SumMonad_262 :: () -> T_Monad_186
d_SumMonad_262 ~()
v0 = T_Monad_186
du_SumMonad_262
du_SumMonad_262 :: T_Monad_186
du_SumMonad_262 :: T_Monad_186
du_SumMonad_262
  = ((() -> AgdaAny -> AgdaAny)
 -> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
 -> T_Monad_186)
-> AgdaAny -> AgdaAny -> T_Monad_186
forall a b. a -> b
coe
      (() -> AgdaAny -> AgdaAny)
-> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> T_Monad_186
C_Monad'46'constructor_12257
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> (AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 -> (T__'8846'__30 -> (AgdaAny -> T__'8846'__30) -> T__'8846'__30)
-> AgdaAny
forall a b. a -> b
coe T__'8846'__30 -> (AgdaAny -> T__'8846'__30) -> T__'8846'__30
du_sumBind_248))
-- Utils.EitherMonad
d_EitherMonad_268 :: () -> T_Monad_186
d_EitherMonad_268 :: () -> T_Monad_186
d_EitherMonad_268 ~()
v0 = T_Monad_186
du_EitherMonad_268
du_EitherMonad_268 :: T_Monad_186
du_EitherMonad_268 :: T_Monad_186
du_EitherMonad_268
  = ((() -> AgdaAny -> AgdaAny)
 -> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
 -> T_Monad_186)
-> AgdaAny -> AgdaAny -> T_Monad_186
forall a b. a -> b
coe
      (() -> AgdaAny -> AgdaAny)
-> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> T_Monad_186
C_Monad'46'constructor_12257 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> (AgdaAny -> T_Either_6 AgdaAny AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Either_6 AgdaAny AgdaAny
forall {a} {b}. b -> Either a b
C_inj'8322'_14))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 -> (T_Either_6 AgdaAny AgdaAny
 -> (AgdaAny -> T_Either_6 AgdaAny AgdaAny)
 -> T_Either_6 AgdaAny AgdaAny)
-> AgdaAny
forall a b. a -> b
coe T_Either_6 AgdaAny AgdaAny
-> (AgdaAny -> T_Either_6 AgdaAny AgdaAny)
-> T_Either_6 AgdaAny AgdaAny
du_eitherBind_42))
-- Utils.EitherP
d_EitherP_274 :: () -> T_Monad_186
d_EitherP_274 :: () -> T_Monad_186
d_EitherP_274 ~()
v0 = T_Monad_186
du_EitherP_274
du_EitherP_274 :: T_Monad_186
du_EitherP_274 :: T_Monad_186
du_EitherP_274
  = ((() -> AgdaAny -> AgdaAny)
 -> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
 -> T_Monad_186)
-> AgdaAny -> AgdaAny -> T_Monad_186
forall a b. a -> b
coe
      (() -> AgdaAny -> AgdaAny)
-> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> T_Monad_186
C_Monad'46'constructor_12257 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> (AgdaAny -> T_Either_6 AgdaAny AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Either_6 AgdaAny AgdaAny
forall {a} {b}. b -> Either a b
C_inj'8322'_14))
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 -> (T_Either_6 AgdaAny AgdaAny
 -> (AgdaAny -> T_Either_6 AgdaAny AgdaAny)
 -> T_Either_6 AgdaAny AgdaAny)
-> AgdaAny
forall a b. a -> b
coe T_Either_6 AgdaAny AgdaAny
-> (AgdaAny -> T_Either_6 AgdaAny AgdaAny)
-> T_Either_6 AgdaAny AgdaAny
du_eitherBind_42))
-- Utils.withE
d_withE_282 ::
  () ->
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  T_Either_6 AgdaAny AgdaAny -> T_Either_6 AgdaAny AgdaAny
d_withE_282 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> T_Either_6 AgdaAny AgdaAny
-> T_Either_6 AgdaAny AgdaAny
d_withE_282 ~()
v0 ~()
v1 ~()
v2 AgdaAny -> AgdaAny
v3 T_Either_6 AgdaAny AgdaAny
v4 = (AgdaAny -> AgdaAny)
-> T_Either_6 AgdaAny AgdaAny -> T_Either_6 AgdaAny AgdaAny
du_withE_282 AgdaAny -> AgdaAny
v3 T_Either_6 AgdaAny AgdaAny
v4
du_withE_282 ::
  (AgdaAny -> AgdaAny) ->
  T_Either_6 AgdaAny AgdaAny -> T_Either_6 AgdaAny AgdaAny
du_withE_282 :: (AgdaAny -> AgdaAny)
-> T_Either_6 AgdaAny AgdaAny -> T_Either_6 AgdaAny AgdaAny
du_withE_282 AgdaAny -> AgdaAny
v0 T_Either_6 AgdaAny AgdaAny
v1
  = case T_Either_6 AgdaAny AgdaAny -> T_Either_6 AgdaAny AgdaAny
forall a b. a -> b
coe T_Either_6 AgdaAny AgdaAny
v1 of
      C_inj'8321'_12 AgdaAny
v2 -> (AgdaAny -> T_Either_6 AgdaAny AgdaAny)
-> AgdaAny -> T_Either_6 AgdaAny AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Either_6 AgdaAny AgdaAny
forall {a} {b}. a -> Either a b
C_inj'8321'_12 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v2)
      C_inj'8322'_14 AgdaAny
v2 -> T_Either_6 AgdaAny AgdaAny -> T_Either_6 AgdaAny AgdaAny
forall a b. a -> b
coe T_Either_6 AgdaAny AgdaAny
v1
      T_Either_6 AgdaAny AgdaAny
_ -> T_Either_6 AgdaAny AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.dec2Either
d_dec2Either_294 ::
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  T_Either_6
    (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) AgdaAny
d_dec2Either_294 :: () -> T_Dec_20 -> T_Either_6 (AgdaAny -> T_Irrelevant_20) AgdaAny
d_dec2Either_294 ~()
v0 T_Dec_20
v1 = T_Dec_20 -> T_Either_6 (AgdaAny -> T_Irrelevant_20) AgdaAny
du_dec2Either_294 T_Dec_20
v1
du_dec2Either_294 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  T_Either_6
    (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) AgdaAny
du_dec2Either_294 :: T_Dec_20 -> T_Either_6 (AgdaAny -> T_Irrelevant_20) AgdaAny
du_dec2Either_294 T_Dec_20
v0
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v1 T_Reflects_16
v2
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
             then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v2 of
                    MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v3
                      -> (AgdaAny -> T_Either_6 AgdaAny AgdaAny)
-> AgdaAny -> T_Either_6 (AgdaAny -> T_Irrelevant_20) AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Either_6 AgdaAny AgdaAny
forall {a} {b}. b -> Either a b
C_inj'8322'_14 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
                    T_Reflects_16
_ -> T_Either_6 (AgdaAny -> T_Irrelevant_20) AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
             else (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Either_6 (AgdaAny -> T_Irrelevant_20) AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2) ((AgdaAny -> T_Either_6 AgdaAny AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Either_6 AgdaAny AgdaAny
forall {a} {b}. a -> Either a b
C_inj'8321'_12 AgdaAny
forall a. a
erased)
      T_Dec_20
_ -> T_Either_6 (AgdaAny -> T_Irrelevant_20) AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.Writer
d_Writer_304 :: p -> p -> ()
d_Writer_304 p
a0 p
a1 = ()
data T_Writer_304 = C__'44'__318 AgdaAny AgdaAny
-- Utils.Writer.wrvalue
d_wrvalue_314 :: T_Writer_304 -> AgdaAny
d_wrvalue_314 :: T_Writer_304 -> AgdaAny
d_wrvalue_314 T_Writer_304
v0
  = case T_Writer_304 -> T_Writer_304
forall a b. a -> b
coe T_Writer_304
v0 of
      C__'44'__318 AgdaAny
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      T_Writer_304
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.Writer.accum
d_accum_316 :: T_Writer_304 -> AgdaAny
d_accum_316 :: T_Writer_304 -> AgdaAny
d_accum_316 T_Writer_304
v0
  = case T_Writer_304 -> T_Writer_304
forall a b. a -> b
coe T_Writer_304
v0 of
      C__'44'__318 AgdaAny
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
      T_Writer_304
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.WriterMonad.WriterMonad
d_WriterMonad_328 ::
  () -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Monad_186
d_WriterMonad_328 :: () -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Monad_186
d_WriterMonad_328 ~()
v0 AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny
v2 = AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Monad_186
du_WriterMonad_328 AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny
v2
du_WriterMonad_328 ::
  AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Monad_186
du_WriterMonad_328 :: AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Monad_186
du_WriterMonad_328 AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny
v1
  = ((() -> AgdaAny -> AgdaAny)
 -> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
 -> T_Monad_186)
-> AgdaAny -> AgdaAny -> T_Monad_186
forall a b. a -> b
coe
      (() -> AgdaAny -> AgdaAny)
-> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> T_Monad_186
C_Monad'46'constructor_12257
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 AgdaAny
v3 -> (AgdaAny -> AgdaAny -> T_Writer_304)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Writer_304
C__'44'__318 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0)))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
            case AgdaAny -> T_Writer_304
forall a b. a -> b
coe AgdaAny
v4 of
              C__'44'__318 AgdaAny
v5 AgdaAny
v6
                -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                     (\ AgdaAny
v7 ->
                        (AgdaAny -> AgdaAny -> T_Writer_304)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          AgdaAny -> AgdaAny -> T_Writer_304
C__'44'__318 ((T_Writer_304 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Writer_304 -> AgdaAny
d_wrvalue_314 (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7 AgdaAny
v5))
                          ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v6 (T_Writer_304 -> AgdaAny
d_accum_316 (AgdaAny -> AgdaAny -> T_Writer_304
forall a b. a -> b
coe AgdaAny
v7 AgdaAny
v5))))
              T_Writer_304
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
-- Utils.WriterMonad.tell
d_tell_344 ::
  () ->
  AgdaAny ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Writer_304
d_tell_344 :: ()
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Writer_304
d_tell_344 ~()
v0 ~AgdaAny
v1 ~AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 = AgdaAny -> T_Writer_304
du_tell_344 AgdaAny
v3
du_tell_344 :: AgdaAny -> T_Writer_304
du_tell_344 :: AgdaAny -> T_Writer_304
du_tell_344 AgdaAny
v0
  = (AgdaAny -> AgdaAny -> T_Writer_304)
-> AgdaAny -> AgdaAny -> T_Writer_304
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Writer_304
C__'44'__318 (() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0)
-- Utils.RuntimeError
d_RuntimeError_348 :: ()
d_RuntimeError_348 = ()
type T_RuntimeError_348 = RuntimeError
pattern $mC_gasError_350 :: forall {r}. RuntimeError -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_gasError_350 :: RuntimeError
C_gasError_350 = GasError
pattern $mC_userError_352 :: forall {r}. RuntimeError -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_userError_352 :: RuntimeError
C_userError_352 = UserError
pattern $mC_runtimeTypeError_354 :: forall {r}. RuntimeError -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_runtimeTypeError_354 :: RuntimeError
C_runtimeTypeError_354 = RuntimeTypeError
check_gasError_350 :: T_RuntimeError_348
check_gasError_350 :: RuntimeError
check_gasError_350 = RuntimeError
GasError
check_userError_352 :: T_RuntimeError_348
check_userError_352 :: RuntimeError
check_userError_352 = RuntimeError
UserError
check_runtimeTypeError_354 :: T_RuntimeError_348
check_runtimeTypeError_354 :: RuntimeError
check_runtimeTypeError_354 = RuntimeError
RuntimeTypeError
cover_RuntimeError_348 :: RuntimeError -> ()
cover_RuntimeError_348 :: RuntimeError -> ()
cover_RuntimeError_348 RuntimeError
x
  = case RuntimeError
x of
      RuntimeError
GasError -> ()
      RuntimeError
UserError -> ()
      RuntimeError
RuntimeTypeError -> ()
-- Utils.ByteString
type T_ByteString_356 = BS.ByteString
d_ByteString_356 :: a
d_ByteString_356
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Utils.ByteString"
-- Utils.eqByteString
d_eqByteString_358 :: T_ByteString_356 -> T_ByteString_356 -> Bool
d_eqByteString_358 :: T_ByteString_356 -> T_ByteString_356 -> Bool
d_eqByteString_358 = T_ByteString_356 -> T_ByteString_356 -> Bool
forall a. Eq a => a -> a -> Bool
(==)
-- Utils._×_
d__'215'__364 :: p -> p -> ()
d__'215'__364 p
a0 p
a1 = ()
type T__'215'__364 a0 a1 = Pair a0 a1
pattern $mC__'44'__378 :: forall {r} {a} {b}. (a, b) -> (a -> b -> r) -> ((# #) -> r) -> r
$bC__'44'__378 :: forall {a} {b}. a -> b -> (a, b)
C__'44'__378 a0 a1 = (,) a0 a1
check__'44'__378 ::
  forall xA. forall xB. xA -> xB -> T__'215'__364 xA xB
check__'44'__378 :: forall {a} {b}. a -> b -> (a, b)
check__'44'__378 = (,)
cover__'215'__364 :: Pair a1 a2 -> ()
cover__'215'__364 :: forall a1 a2. Pair a1 a2 -> ()
cover__'215'__364 Pair a1 a2
x
  = case Pair a1 a2
x of
      (,) a1
_ a2
_ -> ()
-- Utils._×_.proj₁
d_proj'8321'_374 :: T__'215'__364 AgdaAny AgdaAny -> AgdaAny
d_proj'8321'_374 :: T__'215'__364 AgdaAny AgdaAny -> AgdaAny
d_proj'8321'_374 T__'215'__364 AgdaAny AgdaAny
v0
  = case T__'215'__364 AgdaAny AgdaAny -> T__'215'__364 AgdaAny AgdaAny
forall a b. a -> b
coe T__'215'__364 AgdaAny AgdaAny
v0 of
      C__'44'__378 AgdaAny
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      T__'215'__364 AgdaAny AgdaAny
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils._×_.proj₂
d_proj'8322'_376 :: T__'215'__364 AgdaAny AgdaAny -> AgdaAny
d_proj'8322'_376 :: T__'215'__364 AgdaAny AgdaAny -> AgdaAny
d_proj'8322'_376 T__'215'__364 AgdaAny AgdaAny
v0
  = case T__'215'__364 AgdaAny AgdaAny -> T__'215'__364 AgdaAny AgdaAny
forall a b. a -> b
coe T__'215'__364 AgdaAny AgdaAny
v0 of
      C__'44'__378 AgdaAny
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
      T__'215'__364 AgdaAny AgdaAny
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.List
d_List_382 :: p -> ()
d_List_382 p
a0 = ()
type T_List_382 a0 = [] a0
pattern $mC_'91''93'_386 :: forall {r} {a}. [a] -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_'91''93'_386 :: forall {a}. [a]
C_'91''93'_386 = []
pattern $mC__'8759'__388 :: forall {r} {a}. [a] -> (a -> [a] -> r) -> ((# #) -> r) -> r
$bC__'8759'__388 :: forall {a}. a -> [a] -> [a]
C__'8759'__388 a0 a1 = (:) a0 a1
check_'91''93'_386 :: forall xA. T_List_382 xA
check_'91''93'_386 :: forall {a}. [a]
check_'91''93'_386 = []
check__'8759'__388 ::
  forall xA. xA -> T_List_382 xA -> T_List_382 xA
check__'8759'__388 :: forall {a}. a -> [a] -> [a]
check__'8759'__388 = (:)
cover_List_382 :: [] a1 -> ()
cover_List_382 :: forall a1. [a1] -> ()
cover_List_382 [a1]
x
  = case [a1]
x of
      [] -> ()
      (:) a1
_ [a1]
_ -> ()
-- Utils.length
d_length_392 :: () -> T_List_382 AgdaAny -> Integer
d_length_392 :: () -> T_List_382 AgdaAny -> Integer
d_length_392 ~()
v0 T_List_382 AgdaAny
v1 = T_List_382 AgdaAny -> Integer
du_length_392 T_List_382 AgdaAny
v1
du_length_392 :: T_List_382 AgdaAny -> Integer
du_length_392 :: T_List_382 AgdaAny -> Integer
du_length_392 T_List_382 AgdaAny
v0
  = case T_List_382 AgdaAny -> T_List_382 AgdaAny
forall a b. a -> b
coe T_List_382 AgdaAny
v0 of
      T_List_382 AgdaAny
C_'91''93'_386 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      C__'8759'__388 AgdaAny
v1 T_List_382 AgdaAny
v2
        -> (Integer -> Integer -> Integer) -> AgdaAny -> AgdaAny -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ((T_List_382 AgdaAny -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_382 AgdaAny -> Integer
du_length_392 (T_List_382 AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_382 AgdaAny
v2))
      T_List_382 AgdaAny
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.map
d_map_402 ::
  () ->
  () ->
  (AgdaAny -> AgdaAny) -> T_List_382 AgdaAny -> T_List_382 AgdaAny
d_map_402 :: ()
-> ()
-> (AgdaAny -> AgdaAny)
-> T_List_382 AgdaAny
-> T_List_382 AgdaAny
d_map_402 ~()
v0 ~()
v1 AgdaAny -> AgdaAny
v2 T_List_382 AgdaAny
v3 = (AgdaAny -> AgdaAny) -> T_List_382 AgdaAny -> T_List_382 AgdaAny
du_map_402 AgdaAny -> AgdaAny
v2 T_List_382 AgdaAny
v3
du_map_402 ::
  (AgdaAny -> AgdaAny) -> T_List_382 AgdaAny -> T_List_382 AgdaAny
du_map_402 :: (AgdaAny -> AgdaAny) -> T_List_382 AgdaAny -> T_List_382 AgdaAny
du_map_402 AgdaAny -> AgdaAny
v0 T_List_382 AgdaAny
v1
  = case T_List_382 AgdaAny -> T_List_382 AgdaAny
forall a b. a -> b
coe T_List_382 AgdaAny
v1 of
      T_List_382 AgdaAny
C_'91''93'_386 -> T_List_382 AgdaAny -> T_List_382 AgdaAny
forall a b. a -> b
coe T_List_382 AgdaAny
v1
      C__'8759'__388 AgdaAny
v2 T_List_382 AgdaAny
v3
        -> (AgdaAny -> T_List_382 AgdaAny -> T_List_382 AgdaAny)
-> AgdaAny -> AgdaAny -> T_List_382 AgdaAny
forall a b. a -> b
coe
             AgdaAny -> T_List_382 AgdaAny -> T_List_382 AgdaAny
forall {a}. a -> [a] -> [a]
C__'8759'__388 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v2) (((AgdaAny -> AgdaAny) -> T_List_382 AgdaAny -> T_List_382 AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T_List_382 AgdaAny -> T_List_382 AgdaAny
du_map_402 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) (T_List_382 AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_382 AgdaAny
v3))
      T_List_382 AgdaAny
_ -> T_List_382 AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.toList
d_toList_414 :: () -> T_List_382 AgdaAny -> [AgdaAny]
d_toList_414 :: () -> T_List_382 AgdaAny -> T_List_382 AgdaAny
d_toList_414 ~()
v0 T_List_382 AgdaAny
v1 = T_List_382 AgdaAny -> T_List_382 AgdaAny
du_toList_414 T_List_382 AgdaAny
v1
du_toList_414 :: T_List_382 AgdaAny -> [AgdaAny]
du_toList_414 :: T_List_382 AgdaAny -> T_List_382 AgdaAny
du_toList_414 T_List_382 AgdaAny
v0
  = case T_List_382 AgdaAny -> T_List_382 AgdaAny
forall a b. a -> b
coe T_List_382 AgdaAny
v0 of
      T_List_382 AgdaAny
C_'91''93'_386 -> T_List_382 AgdaAny -> T_List_382 AgdaAny
forall a b. a -> b
coe T_List_382 AgdaAny
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16
      C__'8759'__388 AgdaAny
v1 T_List_382 AgdaAny
v2
        -> (AgdaAny -> T_List_382 AgdaAny -> T_List_382 AgdaAny)
-> AgdaAny -> AgdaAny -> T_List_382 AgdaAny
forall a b. a -> b
coe
             AgdaAny -> T_List_382 AgdaAny -> T_List_382 AgdaAny
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
             ((T_List_382 AgdaAny -> T_List_382 AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_382 AgdaAny -> T_List_382 AgdaAny
du_toList_414 (T_List_382 AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_382 AgdaAny
v2))
      T_List_382 AgdaAny
_ -> T_List_382 AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.fromList
d_fromList_422 :: () -> [AgdaAny] -> T_List_382 AgdaAny
d_fromList_422 :: () -> T_List_382 AgdaAny -> T_List_382 AgdaAny
d_fromList_422 ~()
v0 T_List_382 AgdaAny
v1 = T_List_382 AgdaAny -> T_List_382 AgdaAny
du_fromList_422 T_List_382 AgdaAny
v1
du_fromList_422 :: [AgdaAny] -> T_List_382 AgdaAny
du_fromList_422 :: T_List_382 AgdaAny -> T_List_382 AgdaAny
du_fromList_422 T_List_382 AgdaAny
v0
  = case T_List_382 AgdaAny -> T_List_382 AgdaAny
forall a b. a -> b
coe T_List_382 AgdaAny
v0 of
      [] -> T_List_382 AgdaAny -> T_List_382 AgdaAny
forall a b. a -> b
coe T_List_382 AgdaAny
forall {a}. [a]
C_'91''93'_386
      (:) AgdaAny
v1 T_List_382 AgdaAny
v2
        -> (AgdaAny -> T_List_382 AgdaAny -> T_List_382 AgdaAny)
-> AgdaAny -> AgdaAny -> T_List_382 AgdaAny
forall a b. a -> b
coe AgdaAny -> T_List_382 AgdaAny -> T_List_382 AgdaAny
forall {a}. a -> [a] -> [a]
C__'8759'__388 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ((T_List_382 AgdaAny -> T_List_382 AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_382 AgdaAny -> T_List_382 AgdaAny
du_fromList_422 (T_List_382 AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_382 AgdaAny
v2))
      T_List_382 AgdaAny
_ -> T_List_382 AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.map-cong
d_map'45'cong_440 ::
  () ->
  () ->
  [AgdaAny] ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'45'cong_440 :: ()
-> ()
-> T_List_382 AgdaAny
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8801'__12
d_map'45'cong_440 = ()
-> ()
-> T_List_382 AgdaAny
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8801'__12
forall a. a
erased
-- Utils.DATA
d_DATA_450 :: ()
d_DATA_450 = ()
type T_DATA_450 = Data
pattern $mC_ConstrDATA_452 :: forall {r}.
T_DATA_450 -> (Integer -> [T_DATA_450] -> r) -> ((# #) -> r) -> r
$bC_ConstrDATA_452 :: Integer -> [T_DATA_450] -> T_DATA_450
C_ConstrDATA_452 a0 a1 = D.Constr a0 a1
pattern $mC_MapDATA_454 :: forall {r}.
T_DATA_450
-> ([(T_DATA_450, T_DATA_450)] -> r) -> ((# #) -> r) -> r
$bC_MapDATA_454 :: [(T_DATA_450, T_DATA_450)] -> T_DATA_450
C_MapDATA_454 a0 = D.Map a0
pattern $mC_ListDATA_456 :: forall {r}. T_DATA_450 -> ([T_DATA_450] -> r) -> ((# #) -> r) -> r
$bC_ListDATA_456 :: [T_DATA_450] -> T_DATA_450
C_ListDATA_456 a0 = D.List a0
pattern $mC_iDATA_458 :: forall {r}. T_DATA_450 -> (Integer -> r) -> ((# #) -> r) -> r
$bC_iDATA_458 :: Integer -> T_DATA_450
C_iDATA_458 a0 = D.I a0
pattern $mC_bDATA_460 :: forall {r}.
T_DATA_450 -> (T_ByteString_356 -> r) -> ((# #) -> r) -> r
$bC_bDATA_460 :: T_ByteString_356 -> T_DATA_450
C_bDATA_460 a0 = D.B a0
check_ConstrDATA_452 ::
  Integer -> T_List_382 T_DATA_450 -> T_DATA_450
check_ConstrDATA_452 :: Integer -> [T_DATA_450] -> T_DATA_450
check_ConstrDATA_452 = Integer -> [T_DATA_450] -> T_DATA_450
D.Constr
check_MapDATA_454 ::
  T_List_382 (T__'215'__364 T_DATA_450 T_DATA_450) -> T_DATA_450
check_MapDATA_454 :: [(T_DATA_450, T_DATA_450)] -> T_DATA_450
check_MapDATA_454 = [(T_DATA_450, T_DATA_450)] -> T_DATA_450
D.Map
check_ListDATA_456 :: T_List_382 T_DATA_450 -> T_DATA_450
check_ListDATA_456 :: [T_DATA_450] -> T_DATA_450
check_ListDATA_456 = [T_DATA_450] -> T_DATA_450
D.List
check_iDATA_458 :: Integer -> T_DATA_450
check_iDATA_458 :: Integer -> T_DATA_450
check_iDATA_458 = Integer -> T_DATA_450
D.I
check_bDATA_460 :: T_ByteString_356 -> T_DATA_450
check_bDATA_460 :: T_ByteString_356 -> T_DATA_450
check_bDATA_460 = T_ByteString_356 -> T_DATA_450
D.B
cover_DATA_450 :: Data -> ()
cover_DATA_450 :: T_DATA_450 -> ()
cover_DATA_450 T_DATA_450
x
  = case T_DATA_450
x of
      D.Constr Integer
_ [T_DATA_450]
_ -> ()
      D.Map [(T_DATA_450, T_DATA_450)]
_ -> ()
      D.List [T_DATA_450]
_ -> ()
      D.I Integer
_ -> ()
      D.B T_ByteString_356
_ -> ()
-- Utils.eqDATA
d_eqDATA_462 :: T_DATA_450 -> T_DATA_450 -> Bool
d_eqDATA_462 :: T_DATA_450 -> T_DATA_450 -> Bool
d_eqDATA_462 = T_DATA_450 -> T_DATA_450 -> Bool
forall a. Eq a => a -> a -> Bool
(==)
-- Utils.Bls12-381-G1-Element
type T_Bls12'45'381'45'G1'45'Element_464 = G1.Element
d_Bls12'45'381'45'G1'45'Element_464 :: a
d_Bls12'45'381'45'G1'45'Element_464
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Utils.Bls12-381-G1-Element"
-- Utils.eqBls12-381-G1-Element
d_eqBls12'45'381'45'G1'45'Element_466 ::
  T_Bls12'45'381'45'G1'45'Element_464 ->
  T_Bls12'45'381'45'G1'45'Element_464 -> Bool
d_eqBls12'45'381'45'G1'45'Element_466 :: T_Bls12'45'381'45'G1'45'Element_464
-> T_Bls12'45'381'45'G1'45'Element_464 -> Bool
d_eqBls12'45'381'45'G1'45'Element_466 = T_Bls12'45'381'45'G1'45'Element_464
-> T_Bls12'45'381'45'G1'45'Element_464 -> Bool
forall a. Eq a => a -> a -> Bool
(==)
-- Utils.Bls12-381-G2-Element
type T_Bls12'45'381'45'G2'45'Element_468 = G2.Element
d_Bls12'45'381'45'G2'45'Element_468 :: a
d_Bls12'45'381'45'G2'45'Element_468
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Utils.Bls12-381-G2-Element"
-- Utils.eqBls12-381-G2-Element
d_eqBls12'45'381'45'G2'45'Element_470 ::
  T_Bls12'45'381'45'G2'45'Element_468 ->
  T_Bls12'45'381'45'G2'45'Element_468 -> Bool
d_eqBls12'45'381'45'G2'45'Element_470 :: T_Bls12'45'381'45'G2'45'Element_468
-> T_Bls12'45'381'45'G2'45'Element_468 -> Bool
d_eqBls12'45'381'45'G2'45'Element_470 = T_Bls12'45'381'45'G2'45'Element_468
-> T_Bls12'45'381'45'G2'45'Element_468 -> Bool
forall a. Eq a => a -> a -> Bool
(==)
-- Utils.Bls12-381-MlResult
type T_Bls12'45'381'45'MlResult_472 = Pairing.MlResult
d_Bls12'45'381'45'MlResult_472 :: a
d_Bls12'45'381'45'MlResult_472
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Utils.Bls12-381-MlResult"
-- Utils.eqBls12-381-MlResult
d_eqBls12'45'381'45'MlResult_474 ::
  T_Bls12'45'381'45'MlResult_472 ->
  T_Bls12'45'381'45'MlResult_472 -> Bool
d_eqBls12'45'381'45'MlResult_474 :: T_Bls12'45'381'45'MlResult_472
-> T_Bls12'45'381'45'MlResult_472 -> Bool
d_eqBls12'45'381'45'MlResult_474 = T_Bls12'45'381'45'MlResult_472
-> T_Bls12'45'381'45'MlResult_472 -> Bool
forall a. Eq a => a -> a -> Bool
(==)
-- Utils.Kind
d_Kind_476 :: ()
d_Kind_476 = ()
type T_Kind_476 = KIND
pattern $mC_'42'_478 :: forall {r}. KIND -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_'42'_478 :: KIND
C_'42'_478 = Star
pattern $mC_'9839'_480 :: forall {r}. KIND -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_'9839'_480 :: KIND
C_'9839'_480 = Sharp
pattern $mC__'8658'__482 :: forall {r}. KIND -> (KIND -> KIND -> r) -> ((# #) -> r) -> r
$bC__'8658'__482 :: KIND -> KIND -> KIND
C__'8658'__482 a0 a1 = Arrow a0 a1
check_'42'_478 :: T_Kind_476
check_'42'_478 :: KIND
check_'42'_478 = KIND
Star
check_'9839'_480 :: T_Kind_476
check_'9839'_480 :: KIND
check_'9839'_480 = KIND
Sharp
check__'8658'__482 :: T_Kind_476 -> T_Kind_476 -> T_Kind_476
check__'8658'__482 :: KIND -> KIND -> KIND
check__'8658'__482 = KIND -> KIND -> KIND
Arrow
cover_Kind_476 :: KIND -> ()
cover_Kind_476 :: KIND -> ()
cover_Kind_476 KIND
x
  = case KIND
x of
      KIND
Star -> ()
      KIND
Sharp -> ()
      Arrow KIND
_ KIND
_ -> ()