{-# 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.Int
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.Fin.Base
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Nat.Properties
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 qualified Data.Vector.Strict as Strict
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.is-inj₁
d_is'45'inj'8321'_40 ::
  () -> () -> T_Either_6 AgdaAny AgdaAny -> Bool
d_is'45'inj'8321'_40 :: () -> () -> T_Either_6 AgdaAny AgdaAny -> Bool
d_is'45'inj'8321'_40 ~()
v0 ~()
v1 T_Either_6 AgdaAny AgdaAny
v2 = T_Either_6 AgdaAny AgdaAny -> Bool
du_is'45'inj'8321'_40 T_Either_6 AgdaAny AgdaAny
v2
du_is'45'inj'8321'_40 :: T_Either_6 AgdaAny AgdaAny -> Bool
du_is'45'inj'8321'_40 :: T_Either_6 AgdaAny AgdaAny -> Bool
du_is'45'inj'8321'_40 T_Either_6 AgdaAny AgdaAny
v0
  = 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
v1 -> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
      C_inj'8322'_14 AgdaAny
v1 -> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
      T_Either_6 AgdaAny AgdaAny
_ -> Bool
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.is-inj₂
d_is'45'inj'8322'_46 ::
  () -> () -> T_Either_6 AgdaAny AgdaAny -> Bool
d_is'45'inj'8322'_46 :: () -> () -> T_Either_6 AgdaAny AgdaAny -> Bool
d_is'45'inj'8322'_46 ~()
v0 ~()
v1 T_Either_6 AgdaAny AgdaAny
v2 = T_Either_6 AgdaAny AgdaAny -> Bool
du_is'45'inj'8322'_46 T_Either_6 AgdaAny AgdaAny
v2
du_is'45'inj'8322'_46 :: T_Either_6 AgdaAny AgdaAny -> Bool
du_is'45'inj'8322'_46 :: T_Either_6 AgdaAny AgdaAny -> Bool
du_is'45'inj'8322'_46 T_Either_6 AgdaAny AgdaAny
v0
  = 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
v1 -> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
      C_inj'8322'_14 AgdaAny
v1 -> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
      T_Either_6 AgdaAny AgdaAny
_ -> Bool
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.eitherBind
d_eitherBind_54 ::
  () ->
  () ->
  () ->
  T_Either_6 AgdaAny AgdaAny ->
  (AgdaAny -> T_Either_6 AgdaAny AgdaAny) ->
  T_Either_6 AgdaAny AgdaAny
d_eitherBind_54 :: ()
-> ()
-> ()
-> T_Either_6 AgdaAny AgdaAny
-> (AgdaAny -> T_Either_6 AgdaAny AgdaAny)
-> T_Either_6 AgdaAny AgdaAny
d_eitherBind_54 ~()
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_54 T_Either_6 AgdaAny AgdaAny
v3 AgdaAny -> T_Either_6 AgdaAny AgdaAny
v4
du_eitherBind_54 ::
  T_Either_6 AgdaAny AgdaAny ->
  (AgdaAny -> T_Either_6 AgdaAny AgdaAny) ->
  T_Either_6 AgdaAny AgdaAny
du_eitherBind_54 :: T_Either_6 AgdaAny AgdaAny
-> (AgdaAny -> T_Either_6 AgdaAny AgdaAny)
-> T_Either_6 AgdaAny AgdaAny
du_eitherBind_54 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_68 ::
  () ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_decIf_68 :: () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny -> AgdaAny
d_decIf_68 ~()
v0 ~()
v1 T_Dec_20
v2 AgdaAny
v3 AgdaAny
v4 = T_Dec_20 -> AgdaAny -> AgdaAny -> AgdaAny
du_decIf_68 T_Dec_20
v2 AgdaAny
v3 AgdaAny
v4
du_decIf_68 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_decIf_68 :: T_Dec_20 -> AgdaAny -> AgdaAny -> AgdaAny
du_decIf_68 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.maybeToEither
d_maybeToEither_86 ::
  () -> () -> AgdaAny -> Maybe AgdaAny -> T_Either_6 AgdaAny AgdaAny
d_maybeToEither_86 :: () -> () -> AgdaAny -> Maybe AgdaAny -> T_Either_6 AgdaAny AgdaAny
d_maybeToEither_86 ~()
v0 ~()
v1 AgdaAny
v2 = AgdaAny -> Maybe AgdaAny -> T_Either_6 AgdaAny AgdaAny
du_maybeToEither_86 AgdaAny
v2
du_maybeToEither_86 ::
  AgdaAny -> Maybe AgdaAny -> T_Either_6 AgdaAny AgdaAny
du_maybeToEither_86 :: AgdaAny -> Maybe AgdaAny -> T_Either_6 AgdaAny AgdaAny
du_maybeToEither_86 AgdaAny
v0
  = ((AgdaAny -> AgdaAny) -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> Maybe AgdaAny
-> T_Either_6 AgdaAny AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> AgdaAny -> Maybe AgdaAny -> AgdaAny
MAlonzo.Code.Data.Maybe.Base.du_maybe_32 ((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 -> 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 -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0))
-- Utils.try
d_try_94 ::
  () -> () -> Maybe AgdaAny -> AgdaAny -> T_Either_6 AgdaAny AgdaAny
d_try_94 :: () -> () -> Maybe AgdaAny -> AgdaAny -> T_Either_6 AgdaAny AgdaAny
d_try_94 ~()
v0 ~()
v1 Maybe AgdaAny
v2 AgdaAny
v3 = Maybe AgdaAny -> AgdaAny -> T_Either_6 AgdaAny AgdaAny
du_try_94 Maybe AgdaAny
v2 AgdaAny
v3
du_try_94 :: Maybe AgdaAny -> AgdaAny -> T_Either_6 AgdaAny AgdaAny
du_try_94 :: Maybe AgdaAny -> AgdaAny -> T_Either_6 AgdaAny AgdaAny
du_try_94 Maybe AgdaAny
v0 AgdaAny
v1
  = ((AgdaAny -> AgdaAny) -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Either_6 AgdaAny AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> AgdaAny -> Maybe AgdaAny -> AgdaAny
MAlonzo.Code.Data.Maybe.Base.du_maybe_32 ((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 -> 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 -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)) (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v0)
-- Utils.eitherToMaybe
d_eitherToMaybe_104 ::
  () -> () -> T_Either_6 AgdaAny AgdaAny -> Maybe AgdaAny
d_eitherToMaybe_104 :: () -> () -> T_Either_6 AgdaAny AgdaAny -> Maybe AgdaAny
d_eitherToMaybe_104 ~()
v0 ~()
v1 T_Either_6 AgdaAny AgdaAny
v2 = T_Either_6 AgdaAny AgdaAny -> Maybe AgdaAny
du_eitherToMaybe_104 T_Either_6 AgdaAny AgdaAny
v2
du_eitherToMaybe_104 :: T_Either_6 AgdaAny AgdaAny -> Maybe AgdaAny
du_eitherToMaybe_104 :: T_Either_6 AgdaAny AgdaAny -> Maybe AgdaAny
du_eitherToMaybe_104 T_Either_6 AgdaAny AgdaAny
v0
  = 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
v1
        -> Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
      C_inj'8322'_14 AgdaAny
v1
        -> (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 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
      T_Either_6 AgdaAny AgdaAny
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.natToFin
d_natToFin_110 ::
  Integer -> Integer -> Maybe MAlonzo.Code.Data.Fin.Base.T_Fin_10
d_natToFin_110 :: Integer -> Integer -> Maybe T_Fin_10
d_natToFin_110 Integer
v0 Integer
v1
  = let v2 :: AgdaAny
v2
          = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_178
              (\ AgdaAny
v2 ->
                 (Integer -> T__'8804'__22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   Integer -> T__'8804'__22
MAlonzo.Code.Data.Nat.Properties.du_'8804''7495''8658''8804'_2854
                   ((Integer -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1)))
              ((T__'8804'__22 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                 T__'8804'__22 -> AgdaAny
MAlonzo.Code.Data.Nat.Properties.du_'8804''8658''8804''7495'_2866)
              ((Bool -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 Bool -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_T'63'_72
                 ((Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    Integer -> Integer -> Bool
MAlonzo.Code.Data.Nat.Base.d__'8804''7495'__14
                    ((Integer -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1)) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0))) in
    AgdaAny -> Maybe T_Fin_10
forall a b. a -> b
coe
      (case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v2 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 -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                          ((Integer -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.du_fromℕ'60'_52 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
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) (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
         T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Utils.cong₃
d_cong'8323'_152 ::
  () ->
  () ->
  () ->
  () ->
  (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'_152 :: ()
-> ()
-> ()
-> ()
-> (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'_152 = ()
-> ()
-> ()
-> ()
-> (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_174 ::
  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_174 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
d_'8801''45'subst'45'removable_174 = ()
-> ()
-> ()
-> (AgdaAny -> ())
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
-- Utils._∔_≣_
d__'8724'_'8803'__180 :: p -> p -> p -> ()
d__'8724'_'8803'__180 p
a0 p
a1 p
a2 = ()
data T__'8724'_'8803'__180
  = C_start_184 | C_bubble_192 T__'8724'_'8803'__180
-- Utils.unique∔
d_unique'8724'_204 ::
  Integer ->
  Integer ->
  Integer ->
  T__'8724'_'8803'__180 ->
  T__'8724'_'8803'__180 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_unique'8724'_204 :: Integer
-> Integer
-> Integer
-> T__'8724'_'8803'__180
-> T__'8724'_'8803'__180
-> T__'8801'__12
d_unique'8724'_204 = Integer
-> Integer
-> Integer
-> T__'8724'_'8803'__180
-> T__'8724'_'8803'__180
-> T__'8801'__12
forall a. a
erased
-- Utils.+2∔
d_'43'2'8724'_216 ::
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__'8724'_'8803'__180
d_'43'2'8724'_216 :: Integer
-> Integer -> Integer -> T__'8801'__12 -> T__'8724'_'8803'__180
d_'43'2'8724'_216 Integer
v0 ~Integer
v1 ~Integer
v2 ~T__'8801'__12
v3 = Integer -> T__'8724'_'8803'__180
du_'43'2'8724'_216 Integer
v0
du_'43'2'8724'_216 :: Integer -> T__'8724'_'8803'__180
du_'43'2'8724'_216 :: Integer -> T__'8724'_'8803'__180
du_'43'2'8724'_216 Integer
v0
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T__'8724'_'8803'__180 -> T__'8724'_'8803'__180
forall a b. a -> b
coe T__'8724'_'8803'__180
C_start_184
      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'__180
forall a b. a -> b
coe ((T__'8724'_'8803'__180 -> T__'8724'_'8803'__180)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8724'_'8803'__180 -> T__'8724'_'8803'__180
C_bubble_192 ((Integer -> T__'8724'_'8803'__180) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8724'_'8803'__180
du_'43'2'8724'_216 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1)))
-- Utils.∔2+
d_'8724'2'43'_234 ::
  Integer ->
  Integer ->
  Integer ->
  T__'8724'_'8803'__180 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8724'2'43'_234 :: Integer
-> Integer -> Integer -> T__'8724'_'8803'__180 -> T__'8801'__12
d_'8724'2'43'_234 = Integer
-> Integer -> Integer -> T__'8724'_'8803'__180 -> T__'8801'__12
forall a. a
erased
-- Utils.alldone
d_alldone_240 :: Integer -> T__'8724'_'8803'__180
d_alldone_240 :: Integer -> T__'8724'_'8803'__180
d_alldone_240 Integer
v0 = (Integer -> T__'8724'_'8803'__180)
-> AgdaAny -> T__'8724'_'8803'__180
forall a b. a -> b
coe Integer -> T__'8724'_'8803'__180
du_'43'2'8724'_216 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0)
-- Utils.Monad
d_Monad_246 :: p -> ()
d_Monad_246 p
a0 = ()
data T_Monad_246
  = C_constructor_290 (() -> AgdaAny -> AgdaAny)
                      (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-- Utils.Monad.return
d_return_262 :: T_Monad_246 -> () -> AgdaAny -> AgdaAny
d_return_262 :: T_Monad_246 -> () -> AgdaAny -> AgdaAny
d_return_262 T_Monad_246
v0
  = case T_Monad_246 -> T_Monad_246
forall a b. a -> b
coe T_Monad_246
v0 of
      C_constructor_290 () -> AgdaAny -> AgdaAny
v1 () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
v2 -> (() -> AgdaAny -> AgdaAny) -> () -> AgdaAny -> AgdaAny
forall a b. a -> b
coe () -> AgdaAny -> AgdaAny
v1
      T_Monad_246
_ -> () -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.Monad._>>=_
d__'62''62''61'__268 ::
  T_Monad_246 ->
  () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'62''62''61'__268 :: T_Monad_246
-> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'62''62''61'__268 T_Monad_246
v0
  = case T_Monad_246 -> T_Monad_246
forall a b. a -> b
coe T_Monad_246
v0 of
      C_constructor_290 () -> 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_246
_ -> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.Monad._>>_
d__'62''62'__274 ::
  (() -> ()) ->
  T_Monad_246 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d__'62''62'__274 :: (() -> ())
-> T_Monad_246 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d__'62''62'__274 ~() -> ()
v0 T_Monad_246
v1 ~()
v2 ~()
v3 AgdaAny
v4 AgdaAny
v5 = T_Monad_246 -> AgdaAny -> AgdaAny -> AgdaAny
du__'62''62'__274 T_Monad_246
v1 AgdaAny
v4 AgdaAny
v5
du__'62''62'__274 :: T_Monad_246 -> AgdaAny -> AgdaAny -> AgdaAny
du__'62''62'__274 :: T_Monad_246 -> AgdaAny -> AgdaAny -> AgdaAny
du__'62''62'__274 T_Monad_246
v0 AgdaAny
v1 AgdaAny
v2
  = (T_Monad_246
 -> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> T_Monad_246
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe T_Monad_246
-> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'62''62''61'__268 T_Monad_246
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
v1 (\ AgdaAny
v3 -> AgdaAny
v2)
-- Utils.Monad.fmap
d_fmap_284 ::
  (() -> ()) ->
  T_Monad_246 ->
  () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_fmap_284 :: (() -> ())
-> T_Monad_246
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_fmap_284 ~() -> ()
v0 T_Monad_246
v1 ~()
v2 ~()
v3 AgdaAny -> AgdaAny
v4 AgdaAny
v5 = T_Monad_246 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_fmap_284 T_Monad_246
v1 AgdaAny -> AgdaAny
v4 AgdaAny
v5
du_fmap_284 ::
  T_Monad_246 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_fmap_284 :: T_Monad_246 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_fmap_284 T_Monad_246
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = (T_Monad_246
 -> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> T_Monad_246
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
      T_Monad_246
-> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'62''62''61'__268 T_Monad_246
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
v2
      (\ AgdaAny
v3 -> (T_Monad_246 -> () -> AgdaAny -> AgdaAny)
-> T_Monad_246 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monad_246 -> () -> AgdaAny -> AgdaAny
d_return_262 T_Monad_246
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'__294 ::
  (() -> ()) ->
  T_Monad_246 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d__'62''62'__294 :: (() -> ())
-> T_Monad_246 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d__'62''62'__294 ~() -> ()
v0 T_Monad_246
v1 = T_Monad_246 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
du__'62''62'__294 T_Monad_246
v1
du__'62''62'__294 ::
  T_Monad_246 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
du__'62''62'__294 :: T_Monad_246 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
du__'62''62'__294 T_Monad_246
v0 ()
v1 ()
v2 AgdaAny
v3 AgdaAny
v4
  = (T_Monad_246 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monad_246 -> AgdaAny -> AgdaAny -> AgdaAny
du__'62''62'__274 (T_Monad_246 -> AgdaAny
forall a b. a -> b
coe T_Monad_246
v0) AgdaAny
v3 AgdaAny
v4
-- Utils._._>>=_
d__'62''62''61'__296 ::
  T_Monad_246 ->
  () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'62''62''61'__296 :: T_Monad_246
-> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'62''62''61'__296 T_Monad_246
v0 = (T_Monad_246
 -> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> ()
-> ()
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe T_Monad_246
-> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'62''62''61'__268 (T_Monad_246 -> AgdaAny
forall a b. a -> b
coe T_Monad_246
v0)
-- Utils._.fmap
d_fmap_298 ::
  (() -> ()) ->
  T_Monad_246 ->
  () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_fmap_298 :: (() -> ())
-> T_Monad_246
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_fmap_298 ~() -> ()
v0 T_Monad_246
v1 = T_Monad_246
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_fmap_298 T_Monad_246
v1
du_fmap_298 ::
  T_Monad_246 ->
  () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_fmap_298 :: T_Monad_246
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_fmap_298 T_Monad_246
v0 ()
v1 ()
v2 AgdaAny -> AgdaAny
v3 AgdaAny
v4 = (T_Monad_246 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monad_246 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_fmap_284 (T_Monad_246 -> AgdaAny
forall a b. a -> b
coe T_Monad_246
v0) AgdaAny -> AgdaAny
v3 AgdaAny
v4
-- Utils._.return
d_return_300 :: T_Monad_246 -> () -> AgdaAny -> AgdaAny
d_return_300 :: T_Monad_246 -> () -> AgdaAny -> AgdaAny
d_return_300 T_Monad_246
v0 = (T_Monad_246 -> () -> AgdaAny -> AgdaAny)
-> AgdaAny -> () -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monad_246 -> () -> AgdaAny -> AgdaAny
d_return_262 (T_Monad_246 -> AgdaAny
forall a b. a -> b
coe T_Monad_246
v0)
-- Utils.MaybeMonad
d_MaybeMonad_302 :: T_Monad_246
d_MaybeMonad_302 :: T_Monad_246
d_MaybeMonad_302
  = ((() -> AgdaAny -> AgdaAny)
 -> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
 -> T_Monad_246)
-> AgdaAny -> AgdaAny -> T_Monad_246
forall a b. a -> b
coe
      (() -> AgdaAny -> AgdaAny)
-> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> T_Monad_246
C_constructor_290
      ((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_310 ::
  () ->
  () ->
  () ->
  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_310 :: ()
-> ()
-> ()
-> T__'8846'__30
-> (AgdaAny -> T__'8846'__30)
-> T__'8846'__30
d_sumBind_310 ~()
v0 ~()
v1 ~()
v2 T__'8846'__30
v3 AgdaAny -> T__'8846'__30
v4 = T__'8846'__30 -> (AgdaAny -> T__'8846'__30) -> T__'8846'__30
du_sumBind_310 T__'8846'__30
v3 AgdaAny -> T__'8846'__30
v4
du_sumBind_310 ::
  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_310 :: T__'8846'__30 -> (AgdaAny -> T__'8846'__30) -> T__'8846'__30
du_sumBind_310 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_324 :: () -> T_Monad_246
d_SumMonad_324 :: () -> T_Monad_246
d_SumMonad_324 ~()
v0 = T_Monad_246
du_SumMonad_324
du_SumMonad_324 :: T_Monad_246
du_SumMonad_324 :: T_Monad_246
du_SumMonad_324
  = ((() -> AgdaAny -> AgdaAny)
 -> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
 -> T_Monad_246)
-> AgdaAny -> AgdaAny -> T_Monad_246
forall a b. a -> b
coe
      (() -> AgdaAny -> AgdaAny)
-> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> T_Monad_246
C_constructor_290
      ((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_310))
-- Utils.EitherMonad
d_EitherMonad_330 :: () -> T_Monad_246
d_EitherMonad_330 :: () -> T_Monad_246
d_EitherMonad_330 ~()
v0 = T_Monad_246
du_EitherMonad_330
du_EitherMonad_330 :: T_Monad_246
du_EitherMonad_330 :: T_Monad_246
du_EitherMonad_330
  = ((() -> AgdaAny -> AgdaAny)
 -> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
 -> T_Monad_246)
-> AgdaAny -> AgdaAny -> T_Monad_246
forall a b. a -> b
coe
      (() -> AgdaAny -> AgdaAny)
-> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> T_Monad_246
C_constructor_290 ((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_54))
-- Utils.EitherP
d_EitherP_336 :: () -> T_Monad_246
d_EitherP_336 :: () -> T_Monad_246
d_EitherP_336 ~()
v0 = T_Monad_246
du_EitherP_336
du_EitherP_336 :: T_Monad_246
du_EitherP_336 :: T_Monad_246
du_EitherP_336
  = ((() -> AgdaAny -> AgdaAny)
 -> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
 -> T_Monad_246)
-> AgdaAny -> AgdaAny -> T_Monad_246
forall a b. a -> b
coe
      (() -> AgdaAny -> AgdaAny)
-> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> T_Monad_246
C_constructor_290 ((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_54))
-- Utils.withE
d_withE_344 ::
  () ->
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  T_Either_6 AgdaAny AgdaAny -> T_Either_6 AgdaAny AgdaAny
d_withE_344 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> T_Either_6 AgdaAny AgdaAny
-> T_Either_6 AgdaAny AgdaAny
d_withE_344 ~()
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_344 AgdaAny -> AgdaAny
v3 T_Either_6 AgdaAny AgdaAny
v4
du_withE_344 ::
  (AgdaAny -> AgdaAny) ->
  T_Either_6 AgdaAny AgdaAny -> T_Either_6 AgdaAny AgdaAny
du_withE_344 :: (AgdaAny -> AgdaAny)
-> T_Either_6 AgdaAny AgdaAny -> T_Either_6 AgdaAny AgdaAny
du_withE_344 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_356 ::
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  T_Either_6
    (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) AgdaAny
d_dec2Either_356 :: () -> T_Dec_20 -> T_Either_6 (AgdaAny -> T_Irrelevant_20) AgdaAny
d_dec2Either_356 ~()
v0 T_Dec_20
v1 = T_Dec_20 -> T_Either_6 (AgdaAny -> T_Irrelevant_20) AgdaAny
du_dec2Either_356 T_Dec_20
v1
du_dec2Either_356 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  T_Either_6
    (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) AgdaAny
du_dec2Either_356 :: T_Dec_20 -> T_Either_6 (AgdaAny -> T_Irrelevant_20) AgdaAny
du_dec2Either_356 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_366 :: p -> p -> ()
d_Writer_366 p
a0 p
a1 = ()
data T_Writer_366 = C__'44'__380 AgdaAny AgdaAny
-- Utils.Writer.wrvalue
d_wrvalue_376 :: T_Writer_366 -> AgdaAny
d_wrvalue_376 :: T_Writer_366 -> AgdaAny
d_wrvalue_376 T_Writer_366
v0
  = case T_Writer_366 -> T_Writer_366
forall a b. a -> b
coe T_Writer_366
v0 of
      C__'44'__380 AgdaAny
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      T_Writer_366
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.Writer.accum
d_accum_378 :: T_Writer_366 -> AgdaAny
d_accum_378 :: T_Writer_366 -> AgdaAny
d_accum_378 T_Writer_366
v0
  = case T_Writer_366 -> T_Writer_366
forall a b. a -> b
coe T_Writer_366
v0 of
      C__'44'__380 AgdaAny
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
      T_Writer_366
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.WriterMonad.WriterMonad
d_WriterMonad_390 ::
  () -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Monad_246
d_WriterMonad_390 :: () -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Monad_246
d_WriterMonad_390 ~()
v0 AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny
v2 = AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Monad_246
du_WriterMonad_390 AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny
v2
du_WriterMonad_390 ::
  AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Monad_246
du_WriterMonad_390 :: AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Monad_246
du_WriterMonad_390 AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny
v1
  = ((() -> AgdaAny -> AgdaAny)
 -> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
 -> T_Monad_246)
-> AgdaAny -> AgdaAny -> T_Monad_246
forall a b. a -> b
coe
      (() -> AgdaAny -> AgdaAny)
-> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> T_Monad_246
C_constructor_290
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 AgdaAny
v3 -> (AgdaAny -> AgdaAny -> T_Writer_366)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Writer_366
C__'44'__380 (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_366
forall a b. a -> b
coe AgdaAny
v4 of
              C__'44'__380 AgdaAny
v5 AgdaAny
v6
                -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                     (\ AgdaAny
v7 ->
                        (AgdaAny -> AgdaAny -> T_Writer_366)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          AgdaAny -> AgdaAny -> T_Writer_366
C__'44'__380 ((T_Writer_366 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Writer_366 -> AgdaAny
d_wrvalue_376 (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_366 -> AgdaAny
d_accum_378 (AgdaAny -> AgdaAny -> T_Writer_366
forall a b. a -> b
coe AgdaAny
v7 AgdaAny
v5))))
              T_Writer_366
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
-- Utils.WriterMonad.tell
d_tell_406 ::
  () ->
  AgdaAny ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Writer_366
d_tell_406 :: ()
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Writer_366
d_tell_406 ~()
v0 ~AgdaAny
v1 ~AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 = AgdaAny -> T_Writer_366
du_tell_406 AgdaAny
v3
du_tell_406 :: AgdaAny -> T_Writer_366
du_tell_406 :: AgdaAny -> T_Writer_366
du_tell_406 AgdaAny
v0
  = (AgdaAny -> AgdaAny -> T_Writer_366)
-> AgdaAny -> AgdaAny -> T_Writer_366
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Writer_366
C__'44'__380 (() -> 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_410 :: ()
d_RuntimeError_410 = ()
type T_RuntimeError_410 = RuntimeError
pattern $mC_gasError_412 :: forall {r}. RuntimeError -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_gasError_412 :: RuntimeError
C_gasError_412 = GasError
pattern $mC_userError_414 :: forall {r}. RuntimeError -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_userError_414 :: RuntimeError
C_userError_414 = UserError
pattern $mC_runtimeTypeError_416 :: forall {r}. RuntimeError -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_runtimeTypeError_416 :: RuntimeError
C_runtimeTypeError_416 = RuntimeTypeError
check_gasError_412 :: T_RuntimeError_410
check_gasError_412 :: RuntimeError
check_gasError_412 = RuntimeError
GasError
check_userError_414 :: T_RuntimeError_410
check_userError_414 :: RuntimeError
check_userError_414 = RuntimeError
UserError
check_runtimeTypeError_416 :: T_RuntimeError_410
check_runtimeTypeError_416 :: RuntimeError
check_runtimeTypeError_416 = RuntimeError
RuntimeTypeError
cover_RuntimeError_410 :: RuntimeError -> ()
cover_RuntimeError_410 :: RuntimeError -> ()
cover_RuntimeError_410 RuntimeError
x
  = case RuntimeError
x of
      RuntimeError
GasError -> ()
      RuntimeError
UserError -> ()
      RuntimeError
RuntimeTypeError -> ()
-- Utils.ByteString
type T_ByteString_418 = BS.ByteString
d_ByteString_418 :: a
d_ByteString_418
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Utils.ByteString"
-- Utils.mkByteString
d_mkByteString_420 :: a
d_mkByteString_420
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Utils.mkByteString"
-- Utils.eqByteString
d_eqByteString_422 :: T_ByteString_418 -> T_ByteString_418 -> Bool
d_eqByteString_422 :: T_ByteString_418 -> T_ByteString_418 -> Bool
d_eqByteString_422 = T_ByteString_418 -> T_ByteString_418 -> Bool
forall a. Eq a => a -> a -> Bool
(==)
-- Utils._×_
d__'215'__428 :: p -> p -> ()
d__'215'__428 p
a0 p
a1 = ()
type T__'215'__428 a0 a1 = Pair a0 a1
pattern $mC__'44'__442 :: forall {r} {a} {b}. (a, b) -> (a -> b -> r) -> ((# #) -> r) -> r
$bC__'44'__442 :: forall {a} {b}. a -> b -> (a, b)
C__'44'__442 a0 a1 = (,) a0 a1
check__'44'__442 ::
  forall xA. forall xB. xA -> xB -> T__'215'__428 xA xB
check__'44'__442 :: forall {a} {b}. a -> b -> (a, b)
check__'44'__442 = (,)
cover__'215'__428 :: Pair a1 a2 -> ()
cover__'215'__428 :: forall a1 a2. Pair a1 a2 -> ()
cover__'215'__428 Pair a1 a2
x
  = case Pair a1 a2
x of
      (,) a1
_ a2
_ -> ()
-- Utils._×_.proj₁
d_proj'8321'_438 :: T__'215'__428 AgdaAny AgdaAny -> AgdaAny
d_proj'8321'_438 :: T__'215'__428 AgdaAny AgdaAny -> AgdaAny
d_proj'8321'_438 T__'215'__428 AgdaAny AgdaAny
v0
  = case T__'215'__428 AgdaAny AgdaAny -> T__'215'__428 AgdaAny AgdaAny
forall a b. a -> b
coe T__'215'__428 AgdaAny AgdaAny
v0 of
      C__'44'__442 AgdaAny
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      T__'215'__428 AgdaAny AgdaAny
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils._×_.proj₂
d_proj'8322'_440 :: T__'215'__428 AgdaAny AgdaAny -> AgdaAny
d_proj'8322'_440 :: T__'215'__428 AgdaAny AgdaAny -> AgdaAny
d_proj'8322'_440 T__'215'__428 AgdaAny AgdaAny
v0
  = case T__'215'__428 AgdaAny AgdaAny -> T__'215'__428 AgdaAny AgdaAny
forall a b. a -> b
coe T__'215'__428 AgdaAny AgdaAny
v0 of
      C__'44'__442 AgdaAny
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
      T__'215'__428 AgdaAny AgdaAny
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.List
d_List_446 :: p -> ()
d_List_446 p
a0 = ()
type T_List_446 a0 = [] a0
pattern $mC_'91''93'_450 :: forall {r} {a}. [a] -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_'91''93'_450 :: forall {a}. [a]
C_'91''93'_450 = []
pattern $mC__'8759'__452 :: forall {r} {a}. [a] -> (a -> [a] -> r) -> ((# #) -> r) -> r
$bC__'8759'__452 :: forall {a}. a -> [a] -> [a]
C__'8759'__452 a0 a1 = (:) a0 a1
check_'91''93'_450 :: forall xA. T_List_446 xA
check_'91''93'_450 :: forall {a}. [a]
check_'91''93'_450 = []
check__'8759'__452 ::
  forall xA. xA -> T_List_446 xA -> T_List_446 xA
check__'8759'__452 :: forall {a}. a -> [a] -> [a]
check__'8759'__452 = (:)
cover_List_446 :: [] a1 -> ()
cover_List_446 :: forall a1. [a1] -> ()
cover_List_446 [a1]
x
  = case [a1]
x of
      [] -> ()
      (:) a1
_ [a1]
_ -> ()
-- Utils.All
d_All_460 :: p -> p -> p -> p -> ()
d_All_460 p
a0 p
a1 p
a2 p
a3 = ()
data T_All_460 = C_'91''93'_468 | C__'8759'__478 AgdaAny T_All_460
-- Utils.length
d_length_482 :: () -> T_List_446 AgdaAny -> Integer
d_length_482 :: () -> T_List_446 AgdaAny -> Integer
d_length_482 ~()
v0 T_List_446 AgdaAny
v1 = T_List_446 AgdaAny -> Integer
du_length_482 T_List_446 AgdaAny
v1
du_length_482 :: T_List_446 AgdaAny -> Integer
du_length_482 :: T_List_446 AgdaAny -> Integer
du_length_482 T_List_446 AgdaAny
v0
  = case T_List_446 AgdaAny -> T_List_446 AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v0 of
      T_List_446 AgdaAny
C_'91''93'_450 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      C__'8759'__452 AgdaAny
v1 T_List_446 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_446 AgdaAny -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny -> Integer
du_length_482 (T_List_446 AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v2))
      T_List_446 AgdaAny
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.map
d_map_492 ::
  () ->
  () ->
  (AgdaAny -> AgdaAny) -> T_List_446 AgdaAny -> T_List_446 AgdaAny
d_map_492 :: ()
-> ()
-> (AgdaAny -> AgdaAny)
-> T_List_446 AgdaAny
-> T_List_446 AgdaAny
d_map_492 ~()
v0 ~()
v1 AgdaAny -> AgdaAny
v2 T_List_446 AgdaAny
v3 = (AgdaAny -> AgdaAny) -> T_List_446 AgdaAny -> T_List_446 AgdaAny
du_map_492 AgdaAny -> AgdaAny
v2 T_List_446 AgdaAny
v3
du_map_492 ::
  (AgdaAny -> AgdaAny) -> T_List_446 AgdaAny -> T_List_446 AgdaAny
du_map_492 :: (AgdaAny -> AgdaAny) -> T_List_446 AgdaAny -> T_List_446 AgdaAny
du_map_492 AgdaAny -> AgdaAny
v0 T_List_446 AgdaAny
v1
  = case T_List_446 AgdaAny -> T_List_446 AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v1 of
      T_List_446 AgdaAny
C_'91''93'_450 -> T_List_446 AgdaAny -> T_List_446 AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v1
      C__'8759'__452 AgdaAny
v2 T_List_446 AgdaAny
v3
        -> (AgdaAny -> T_List_446 AgdaAny -> T_List_446 AgdaAny)
-> AgdaAny -> AgdaAny -> T_List_446 AgdaAny
forall a b. a -> b
coe
             AgdaAny -> T_List_446 AgdaAny -> T_List_446 AgdaAny
forall {a}. a -> [a] -> [a]
C__'8759'__452 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v2) (((AgdaAny -> AgdaAny) -> T_List_446 AgdaAny -> T_List_446 AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T_List_446 AgdaAny -> T_List_446 AgdaAny
du_map_492 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) (T_List_446 AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v3))
      T_List_446 AgdaAny
_ -> T_List_446 AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.toList
d_toList_504 :: () -> T_List_446 AgdaAny -> [AgdaAny]
d_toList_504 :: () -> T_List_446 AgdaAny -> T_List_446 AgdaAny
d_toList_504 ~()
v0 T_List_446 AgdaAny
v1 = T_List_446 AgdaAny -> T_List_446 AgdaAny
du_toList_504 T_List_446 AgdaAny
v1
du_toList_504 :: T_List_446 AgdaAny -> [AgdaAny]
du_toList_504 :: T_List_446 AgdaAny -> T_List_446 AgdaAny
du_toList_504 T_List_446 AgdaAny
v0
  = case T_List_446 AgdaAny -> T_List_446 AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v0 of
      T_List_446 AgdaAny
C_'91''93'_450 -> T_List_446 AgdaAny -> T_List_446 AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16
      C__'8759'__452 AgdaAny
v1 T_List_446 AgdaAny
v2
        -> (AgdaAny -> T_List_446 AgdaAny -> T_List_446 AgdaAny)
-> AgdaAny -> AgdaAny -> T_List_446 AgdaAny
forall a b. a -> b
coe
             AgdaAny -> T_List_446 AgdaAny -> T_List_446 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_446 AgdaAny -> T_List_446 AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny -> T_List_446 AgdaAny
du_toList_504 (T_List_446 AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v2))
      T_List_446 AgdaAny
_ -> T_List_446 AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.fromList
d_fromList_512 :: () -> [AgdaAny] -> T_List_446 AgdaAny
d_fromList_512 :: () -> T_List_446 AgdaAny -> T_List_446 AgdaAny
d_fromList_512 ~()
v0 T_List_446 AgdaAny
v1 = T_List_446 AgdaAny -> T_List_446 AgdaAny
du_fromList_512 T_List_446 AgdaAny
v1
du_fromList_512 :: [AgdaAny] -> T_List_446 AgdaAny
du_fromList_512 :: T_List_446 AgdaAny -> T_List_446 AgdaAny
du_fromList_512 T_List_446 AgdaAny
v0
  = case T_List_446 AgdaAny -> T_List_446 AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v0 of
      [] -> T_List_446 AgdaAny -> T_List_446 AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
forall {a}. [a]
C_'91''93'_450
      (:) AgdaAny
v1 T_List_446 AgdaAny
v2
        -> (AgdaAny -> T_List_446 AgdaAny -> T_List_446 AgdaAny)
-> AgdaAny -> AgdaAny -> T_List_446 AgdaAny
forall a b. a -> b
coe AgdaAny -> T_List_446 AgdaAny -> T_List_446 AgdaAny
forall {a}. a -> [a] -> [a]
C__'8759'__452 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ((T_List_446 AgdaAny -> T_List_446 AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny -> T_List_446 AgdaAny
du_fromList_512 (T_List_446 AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v2))
      T_List_446 AgdaAny
_ -> T_List_446 AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.dropLIST
d_dropLIST_520 ::
  () -> Integer -> T_List_446 AgdaAny -> T_List_446 AgdaAny
d_dropLIST_520 :: () -> Integer -> T_List_446 AgdaAny -> T_List_446 AgdaAny
d_dropLIST_520 ~()
v0 Integer
v1 T_List_446 AgdaAny
v2 = Integer -> T_List_446 AgdaAny -> T_List_446 AgdaAny
du_dropLIST_520 Integer
v1 T_List_446 AgdaAny
v2
du_dropLIST_520 ::
  Integer -> T_List_446 AgdaAny -> T_List_446 AgdaAny
du_dropLIST_520 :: Integer -> T_List_446 AgdaAny -> T_List_446 AgdaAny
du_dropLIST_520 Integer
v0 T_List_446 AgdaAny
v1
  = case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0 of
      AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer)) ->
          (Integer -> T_List_446 AgdaAny -> T_List_446 AgdaAny)
-> AgdaAny -> AgdaAny -> T_List_446 AgdaAny
forall a b. a -> b
coe Integer -> T_List_446 AgdaAny -> T_List_446 AgdaAny
du_drop_532 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0) (T_List_446 AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v1)
      AgdaAny
_ -> T_List_446 AgdaAny -> T_List_446 AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v1
-- Utils._.drop
d_drop_532 ::
  () ->
  Integer ->
  T_List_446 AgdaAny ->
  () -> Integer -> T_List_446 AgdaAny -> T_List_446 AgdaAny
d_drop_532 :: ()
-> Integer
-> T_List_446 AgdaAny
-> ()
-> Integer
-> T_List_446 AgdaAny
-> T_List_446 AgdaAny
d_drop_532 ~()
v0 ~Integer
v1 ~T_List_446 AgdaAny
v2 ~()
v3 Integer
v4 T_List_446 AgdaAny
v5 = Integer -> T_List_446 AgdaAny -> T_List_446 AgdaAny
du_drop_532 Integer
v4 T_List_446 AgdaAny
v5
du_drop_532 :: Integer -> T_List_446 AgdaAny -> T_List_446 AgdaAny
du_drop_532 :: Integer -> T_List_446 AgdaAny -> T_List_446 AgdaAny
du_drop_532 Integer
v0 T_List_446 AgdaAny
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T_List_446 AgdaAny -> T_List_446 AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v1
      Integer
_ -> let v2 :: Integer
v2 = 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_List_446 AgdaAny
forall a b. a -> b
coe
             (case T_List_446 AgdaAny -> T_List_446 AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v1 of
                T_List_446 AgdaAny
C_'91''93'_450 -> T_List_446 AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v1
                C__'8759'__452 AgdaAny
v3 T_List_446 AgdaAny
v4 -> (Integer -> T_List_446 AgdaAny -> T_List_446 AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T_List_446 AgdaAny -> T_List_446 AgdaAny
du_drop_532 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (T_List_446 AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v4)
                T_List_446 AgdaAny
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Utils.map-cong
d_map'45'cong_556 ::
  () ->
  () ->
  [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_556 :: ()
-> ()
-> T_List_446 AgdaAny
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8801'__12
d_map'45'cong_556 = ()
-> ()
-> T_List_446 AgdaAny
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T__'8801'__12)
-> T__'8801'__12
forall a. a
erased
-- Utils.sequence
d_sequence_572 ::
  () -> (() -> ()) -> T_Monad_246 -> T_List_446 AgdaAny -> AgdaAny
d_sequence_572 :: () -> (() -> ()) -> T_Monad_246 -> T_List_446 AgdaAny -> AgdaAny
d_sequence_572 ~()
v0 ~() -> ()
v1 T_Monad_246
v2 T_List_446 AgdaAny
v3 = T_Monad_246 -> T_List_446 AgdaAny -> AgdaAny
du_sequence_572 T_Monad_246
v2 T_List_446 AgdaAny
v3
du_sequence_572 :: T_Monad_246 -> T_List_446 AgdaAny -> AgdaAny
du_sequence_572 :: T_Monad_246 -> T_List_446 AgdaAny -> AgdaAny
du_sequence_572 T_Monad_246
v0 T_List_446 AgdaAny
v1
  = case T_List_446 AgdaAny -> T_List_446 AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v1 of
      T_List_446 AgdaAny
C_'91''93'_450 -> (T_Monad_246 -> () -> AgdaAny -> AgdaAny)
-> T_Monad_246 -> AgdaAny -> T_List_446 AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monad_246 -> () -> AgdaAny -> AgdaAny
d_return_262 T_Monad_246
v0 AgdaAny
forall a. a
erased T_List_446 AgdaAny
v1
      C__'8759'__452 AgdaAny
v2 T_List_446 AgdaAny
v3
        -> (T_Monad_246
 -> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> T_Monad_246
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
             T_Monad_246
-> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'62''62''61'__268 T_Monad_246
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
v2
             (\ AgdaAny
v4 ->
                (T_Monad_246
 -> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> T_Monad_246
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
                  T_Monad_246
-> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'62''62''61'__268 T_Monad_246
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
                  ((T_Monad_246 -> T_List_446 AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monad_246 -> T_List_446 AgdaAny -> AgdaAny
du_sequence_572 (T_Monad_246 -> AgdaAny
forall a b. a -> b
coe T_Monad_246
v0) (T_List_446 AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v3))
                  (\ AgdaAny
v5 ->
                     (T_Monad_246 -> () -> AgdaAny -> AgdaAny)
-> T_Monad_246 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monad_246 -> () -> AgdaAny -> AgdaAny
d_return_262 T_Monad_246
v0 AgdaAny
forall a. a
erased ((AgdaAny -> T_List_446 AgdaAny -> T_List_446 AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_List_446 AgdaAny -> T_List_446 AgdaAny
forall {a}. a -> [a] -> [a]
C__'8759'__452 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))))
      T_List_446 AgdaAny
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Utils.mapM
d_mapM_590 ::
  () ->
  () ->
  (() -> ()) ->
  T_Monad_246 ->
  (AgdaAny -> AgdaAny) -> T_List_446 AgdaAny -> AgdaAny
d_mapM_590 :: ()
-> ()
-> (() -> ())
-> T_Monad_246
-> (AgdaAny -> AgdaAny)
-> T_List_446 AgdaAny
-> AgdaAny
d_mapM_590 ~()
v0 ~()
v1 ~() -> ()
v2 T_Monad_246
v3 AgdaAny -> AgdaAny
v4 T_List_446 AgdaAny
v5 = T_Monad_246
-> (AgdaAny -> AgdaAny) -> T_List_446 AgdaAny -> AgdaAny
du_mapM_590 T_Monad_246
v3 AgdaAny -> AgdaAny
v4 T_List_446 AgdaAny
v5
du_mapM_590 ::
  T_Monad_246 ->
  (AgdaAny -> AgdaAny) -> T_List_446 AgdaAny -> AgdaAny
du_mapM_590 :: T_Monad_246
-> (AgdaAny -> AgdaAny) -> T_List_446 AgdaAny -> AgdaAny
du_mapM_590 T_Monad_246
v0 AgdaAny -> AgdaAny
v1 T_List_446 AgdaAny
v2
  = (T_Monad_246 -> T_List_446 AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Monad_246 -> T_List_446 AgdaAny -> AgdaAny
du_sequence_572 (T_Monad_246 -> AgdaAny
forall a b. a -> b
coe T_Monad_246
v0) (((AgdaAny -> AgdaAny) -> T_List_446 AgdaAny -> T_List_446 AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T_List_446 AgdaAny -> T_List_446 AgdaAny
du_map_492 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (T_List_446 AgdaAny -> AgdaAny
forall a b. a -> b
coe T_List_446 AgdaAny
v2))
-- Utils.Array
type T_Array_594 a0 = Strict.Vector a0
d_Array_594 :: a
d_Array_594
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"MAlonzo Runtime Error: postulate evaluated: Utils.Array"
-- Utils.HSlengthOfArray
d_HSlengthOfArray_598 :: forall xA. () -> T_Array_594 xA -> Integer
d_HSlengthOfArray_598 :: forall xA. () -> T_Array_594 xA -> Integer
d_HSlengthOfArray_598 = \() -> \T_Array_594 xA
as -> Int -> Integer
forall a. Integral a => a -> Integer
toInteger (T_Array_594 xA -> Int
forall a. Vector a -> Int
Strict.length T_Array_594 xA
as)
-- Utils.HSlistToArray
d_HSlistToArray_602 ::
  forall xA. () -> T_List_446 xA -> T_Array_594 xA
d_HSlistToArray_602 :: forall xA. () -> T_List_446 xA -> T_Array_594 xA
d_HSlistToArray_602 = \() -> T_List_446 xA -> T_Array_594 xA
forall a. [a] -> Vector a
Strict.fromList
-- Utils.HSindexArray
d_HSindexArray_604 ::
  forall xA. () -> T_Array_594 xA -> Integer -> xA
d_HSindexArray_604 :: forall xA. () -> T_Array_594 xA -> Integer -> xA
d_HSindexArray_604
  = \() -> \T_Array_594 xA
as -> \Integer
i -> T_Array_594 xA
as T_Array_594 xA -> Int -> xA
forall a. Vector a -> Int -> a
Strict.! (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i)
-- Utils.mkArray
d_mkArray_608 :: a
d_mkArray_608
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"MAlonzo Runtime Error: postulate evaluated: Utils.mkArray"
-- Utils.DATA
d_DATA_610 :: ()
d_DATA_610 = ()
type T_DATA_610 = Data
pattern $mC_ConstrDATA_612 :: forall {r}.
T_DATA_610 -> (Integer -> [T_DATA_610] -> r) -> ((# #) -> r) -> r
$bC_ConstrDATA_612 :: Integer -> [T_DATA_610] -> T_DATA_610
C_ConstrDATA_612 a0 a1 = D.Constr a0 a1
pattern $mC_MapDATA_614 :: forall {r}.
T_DATA_610
-> ([(T_DATA_610, T_DATA_610)] -> r) -> ((# #) -> r) -> r
$bC_MapDATA_614 :: [(T_DATA_610, T_DATA_610)] -> T_DATA_610
C_MapDATA_614 a0 = D.Map a0
pattern $mC_ListDATA_616 :: forall {r}. T_DATA_610 -> ([T_DATA_610] -> r) -> ((# #) -> r) -> r
$bC_ListDATA_616 :: [T_DATA_610] -> T_DATA_610
C_ListDATA_616 a0 = D.List a0
pattern $mC_iDATA_618 :: forall {r}. T_DATA_610 -> (Integer -> r) -> ((# #) -> r) -> r
$bC_iDATA_618 :: Integer -> T_DATA_610
C_iDATA_618 a0 = D.I a0
pattern $mC_bDATA_620 :: forall {r}.
T_DATA_610 -> (T_ByteString_418 -> r) -> ((# #) -> r) -> r
$bC_bDATA_620 :: T_ByteString_418 -> T_DATA_610
C_bDATA_620 a0 = D.B a0
check_ConstrDATA_612 ::
  Integer -> T_List_446 T_DATA_610 -> T_DATA_610
check_ConstrDATA_612 :: Integer -> [T_DATA_610] -> T_DATA_610
check_ConstrDATA_612 = Integer -> [T_DATA_610] -> T_DATA_610
D.Constr
check_MapDATA_614 ::
  T_List_446 (T__'215'__428 T_DATA_610 T_DATA_610) -> T_DATA_610
check_MapDATA_614 :: [(T_DATA_610, T_DATA_610)] -> T_DATA_610
check_MapDATA_614 = [(T_DATA_610, T_DATA_610)] -> T_DATA_610
D.Map
check_ListDATA_616 :: T_List_446 T_DATA_610 -> T_DATA_610
check_ListDATA_616 :: [T_DATA_610] -> T_DATA_610
check_ListDATA_616 = [T_DATA_610] -> T_DATA_610
D.List
check_iDATA_618 :: Integer -> T_DATA_610
check_iDATA_618 :: Integer -> T_DATA_610
check_iDATA_618 = Integer -> T_DATA_610
D.I
check_bDATA_620 :: T_ByteString_418 -> T_DATA_610
check_bDATA_620 :: T_ByteString_418 -> T_DATA_610
check_bDATA_620 = T_ByteString_418 -> T_DATA_610
D.B
cover_DATA_610 :: Data -> ()
cover_DATA_610 :: T_DATA_610 -> ()
cover_DATA_610 T_DATA_610
x
  = case T_DATA_610
x of
      D.Constr Integer
_ [T_DATA_610]
_ -> ()
      D.Map [(T_DATA_610, T_DATA_610)]
_ -> ()
      D.List [T_DATA_610]
_ -> ()
      D.I Integer
_ -> ()
      D.B T_ByteString_418
_ -> ()
-- Utils.eqDATA
d_eqDATA_622 :: T_DATA_610 -> T_DATA_610 -> Bool
d_eqDATA_622 :: T_DATA_610 -> T_DATA_610 -> Bool
d_eqDATA_622 = T_DATA_610 -> T_DATA_610 -> Bool
forall a. Eq a => a -> a -> Bool
(==)
-- Utils.Bls12-381-G1-Element
type T_Bls12'45'381'45'G1'45'Element_756 = G1.Element
d_Bls12'45'381'45'G1'45'Element_756 :: a
d_Bls12'45'381'45'G1'45'Element_756
  = [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_758 ::
  T_Bls12'45'381'45'G1'45'Element_756 ->
  T_Bls12'45'381'45'G1'45'Element_756 -> Bool
d_eqBls12'45'381'45'G1'45'Element_758 :: T_Bls12'45'381'45'G1'45'Element_756
-> T_Bls12'45'381'45'G1'45'Element_756 -> Bool
d_eqBls12'45'381'45'G1'45'Element_758 = T_Bls12'45'381'45'G1'45'Element_756
-> T_Bls12'45'381'45'G1'45'Element_756 -> Bool
forall a. Eq a => a -> a -> Bool
(==)
-- Utils.Bls12-381-G2-Element
type T_Bls12'45'381'45'G2'45'Element_760 = G2.Element
d_Bls12'45'381'45'G2'45'Element_760 :: a
d_Bls12'45'381'45'G2'45'Element_760
  = [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_762 ::
  T_Bls12'45'381'45'G2'45'Element_760 ->
  T_Bls12'45'381'45'G2'45'Element_760 -> Bool
d_eqBls12'45'381'45'G2'45'Element_762 :: T_Bls12'45'381'45'G2'45'Element_760
-> T_Bls12'45'381'45'G2'45'Element_760 -> Bool
d_eqBls12'45'381'45'G2'45'Element_762 = T_Bls12'45'381'45'G2'45'Element_760
-> T_Bls12'45'381'45'G2'45'Element_760 -> Bool
forall a. Eq a => a -> a -> Bool
(==)
-- Utils.Bls12-381-MlResult
type T_Bls12'45'381'45'MlResult_764 = Pairing.MlResult
d_Bls12'45'381'45'MlResult_764 :: a
d_Bls12'45'381'45'MlResult_764
  = [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_766 ::
  T_Bls12'45'381'45'MlResult_764 ->
  T_Bls12'45'381'45'MlResult_764 -> Bool
d_eqBls12'45'381'45'MlResult_766 :: T_Bls12'45'381'45'MlResult_764
-> T_Bls12'45'381'45'MlResult_764 -> Bool
d_eqBls12'45'381'45'MlResult_766 = T_Bls12'45'381'45'MlResult_764
-> T_Bls12'45'381'45'MlResult_764 -> Bool
forall a. Eq a => a -> a -> Bool
(==)
-- Utils.Kind
d_Kind_768 :: ()
d_Kind_768 = ()
type T_Kind_768 = KIND
pattern $mC_'42'_770 :: forall {r}. KIND -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_'42'_770 :: KIND
C_'42'_770 = Star
pattern $mC_'9839'_772 :: forall {r}. KIND -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_'9839'_772 :: KIND
C_'9839'_772 = Sharp
pattern $mC__'8658'__774 :: forall {r}. KIND -> (KIND -> KIND -> r) -> ((# #) -> r) -> r
$bC__'8658'__774 :: KIND -> KIND -> KIND
C__'8658'__774 a0 a1 = Arrow a0 a1
check_'42'_770 :: T_Kind_768
check_'42'_770 :: KIND
check_'42'_770 = KIND
Star
check_'9839'_772 :: T_Kind_768
check_'9839'_772 :: KIND
check_'9839'_772 = KIND
Sharp
check__'8658'__774 :: T_Kind_768 -> T_Kind_768 -> T_Kind_768
check__'8658'__774 :: KIND -> KIND -> KIND
check__'8658'__774 = KIND -> KIND -> KIND
Arrow
cover_Kind_768 :: KIND -> ()
cover_Kind_768 :: KIND -> ()
cover_Kind_768 KIND
x
  = case KIND
x of
      KIND
Star -> ()
      KIND
Sharp -> ()
      Arrow KIND
_ KIND
_ -> ()