{-# 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.Untyped 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.List
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Nat
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Builtin.Constant.AtomicType
import qualified MAlonzo.Code.Builtin.Signature
import qualified MAlonzo.Code.Data.Bool.Base
import qualified MAlonzo.Code.Data.Integer.Show
import qualified MAlonzo.Code.Data.Nat.Properties
import qualified MAlonzo.Code.Data.Nat.Show
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Scoped
import qualified MAlonzo.Code.Utils

import qualified Data.Text as T
-- Untyped._⊢
d__'8866'_14 :: p -> ()
d__'8866'_14 p
a0 = ()
data T__'8866'_14
  = C_'96'_18 AgdaAny | C_ƛ_20 T__'8866'_14 |
    C__'183'__22 T__'8866'_14 T__'8866'_14 | C_force_24 T__'8866'_14 |
    C_delay_26 T__'8866'_14 | C_con_28 MAlonzo.Code.RawU.T_TmCon_198 |
    C_constr_34 Integer [T__'8866'_14] |
    C_case_40 T__'8866'_14 [T__'8866'_14] |
    C_builtin_44 MAlonzo.Code.Builtin.T_Builtin_2 | C_error_46
-- Untyped.uglyDATA
d_uglyDATA_64 ::
  MAlonzo.Code.Utils.T_DATA_450 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_uglyDATA_64 :: T_DATA_450 -> Text
d_uglyDATA_64 ~T_DATA_450
v0 = Text
du_uglyDATA_64
du_uglyDATA_64 :: MAlonzo.Code.Agda.Builtin.String.T_String_6
du_uglyDATA_64 :: Text
du_uglyDATA_64 = Text -> Text
forall a b. a -> b
coe (Text
"(DATA)" :: Data.Text.Text)
-- Untyped.uglyTmCon
d_uglyTmCon_68 ::
  MAlonzo.Code.RawU.T_TmCon_198 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_uglyTmCon_68 :: T_TmCon_198 -> Text
d_uglyTmCon_68 T_TmCon_198
v0
  = case T_TmCon_198 -> T_TmCon_198
forall a b. a -> b
coe T_TmCon_198
v0 of
      MAlonzo.Code.RawU.C_tmCon_202 T__'8866''9839'_4
v1 AgdaAny
v2
        -> case T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe T__'8866''9839'_4
v1 of
             MAlonzo.Code.Builtin.Signature.C_atomic_12 T_AtomicTyCon_6
v4
               -> case T_AtomicTyCon_6 -> T_AtomicTyCon_6
forall a b. a -> b
coe T_AtomicTyCon_6
v4 of
                    T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aInteger_8
                      -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
                           Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                           (Text
"(integer " :: Data.Text.Text)
                           ((Text -> Text -> Text) -> Text -> Text -> AgdaAny
forall a b. a -> b
coe
                              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                              (Integer -> Text
MAlonzo.Code.Data.Integer.Show.d_show_6 (AgdaAny -> Integer
forall a b. a -> b
coe AgdaAny
v2))
                              (Text
")" :: Data.Text.Text))
                    T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBytestring_10
                      -> Text -> Text
forall a b. a -> b
coe (Text
"bytestring" :: Data.Text.Text)
                    T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aString_12
                      -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
                           Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                           (Text
"(string " :: Data.Text.Text)
                           ((Text -> Text -> Text) -> AgdaAny -> Text -> AgdaAny
forall a b. a -> b
coe
                              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20 AgdaAny
v2
                              (Text
")" :: Data.Text.Text))
                    T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aUnit_14
                      -> Text -> Text
forall a b. a -> b
coe (Text
"()" :: Data.Text.Text)
                    T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBool_16
                      -> if AgdaAny -> Bool
forall a b. a -> b
coe AgdaAny
v2
                           then (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
                                  Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                  (Text
"(bool " :: Data.Text.Text)
                                  ((Text -> Text -> Text) -> Text -> Text -> AgdaAny
forall a b. a -> b
coe
                                     Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                     (Text
"true" :: Data.Text.Text) (Text
")" :: Data.Text.Text))
                           else (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
                                  Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                  (Text
"(bool " :: Data.Text.Text)
                                  ((Text -> Text -> Text) -> Text -> Text -> AgdaAny
forall a b. a -> b
coe
                                     Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                     (Text
"false" :: Data.Text.Text) (Text
")" :: Data.Text.Text))
                    T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aData_18
                      -> Text -> Text
forall a b. a -> b
coe Text
du_uglyDATA_64
                    T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'g1'45'element_20
                      -> Text -> Text
forall a b. a -> b
coe (Text
"(bls12-381-g1-element ???)" :: Data.Text.Text)
                    T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'g2'45'element_22
                      -> Text -> Text
forall a b. a -> b
coe (Text
"(bls12-381-g2-element ???)" :: Data.Text.Text)
                    T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'mlresult_24
                      -> Text -> Text
forall a b. a -> b
coe (Text
"(bls12-381-mlresult ???)" :: Data.Text.Text)
                    T_AtomicTyCon_6
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
             MAlonzo.Code.Builtin.Signature.C_list_16 T__'8866''9839'_4
v4
               -> Text -> Text
forall a b. a -> b
coe (Text
"(list [ something ])" :: Data.Text.Text)
             MAlonzo.Code.Builtin.Signature.C_pair_20 T__'8866''9839'_4
v4 T__'8866''9839'_4
v5
               -> case AgdaAny -> (AgdaAny, AgdaAny)
forall a b. a -> b
coe AgdaAny
v2 of
                    MAlonzo.Code.Utils.C__'44'__378 AgdaAny
v6 AgdaAny
v7
                      -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
                           Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                           (Text
"(pair " :: Data.Text.Text)
                           ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                              (T_TmCon_198 -> Text
d_uglyTmCon_68
                                 ((T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198)
-> AgdaAny -> AgdaAny -> T_TmCon_198
forall a b. a -> b
coe T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198
MAlonzo.Code.RawU.C_tmCon_202 (T__'8866''9839'_4 -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)))
                              ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                 (Text
" " :: Data.Text.Text)
                                 ((Text -> Text -> Text) -> Text -> Text -> AgdaAny
forall a b. a -> b
coe
                                    Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                    (T_TmCon_198 -> Text
d_uglyTmCon_68
                                       ((T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198)
-> AgdaAny -> AgdaAny -> T_TmCon_198
forall a b. a -> b
coe T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198
MAlonzo.Code.RawU.C_tmCon_202 (T__'8866''9839'_4 -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7)))
                                    (Text
")" :: Data.Text.Text))))
                    (AgdaAny, AgdaAny)
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8866''9839'_4
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_TmCon_198
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.showNat
d_showNat_96 ::
  Integer -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showNat_96 :: Integer -> Text
d_showNat_96 = String -> Text
T.pack (String -> Text) -> (Integer -> String) -> Integer -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String
forall a. Show a => a -> String
show
-- Untyped.uglyBuiltin
d_uglyBuiltin_98 ::
  MAlonzo.Code.Builtin.T_Builtin_2 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_uglyBuiltin_98 :: T_Builtin_2 -> Text
d_uglyBuiltin_98 T_Builtin_2
v0
  = let v1 :: Text
v1 = Text
"other" :: Data.Text.Text in
    AgdaAny -> Text
forall a b. a -> b
coe
      (case T_Builtin_2 -> T_Builtin_2
forall a b. a -> b
coe T_Builtin_2
v0 of
         T_Builtin_2
MAlonzo.Code.Builtin.C_addInteger_4
           -> Text -> AgdaAny
forall a b. a -> b
coe (Text
"addInteger" :: Data.Text.Text)
         T_Builtin_2
_ -> Text -> AgdaAny
forall a b. a -> b
coe Text
v1)
-- Untyped.uglyList
d_uglyList_102 ::
  () -> [T__'8866'_14] -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_uglyList_102 :: () -> [T__'8866'_14] -> Text
d_uglyList_102 ~()
v0 [T__'8866'_14]
v1 = [T__'8866'_14] -> Text
du_uglyList_102 [T__'8866'_14]
v1
du_uglyList_102 ::
  [T__'8866'_14] -> MAlonzo.Code.Agda.Builtin.String.T_String_6
du_uglyList_102 :: [T__'8866'_14] -> Text
du_uglyList_102 [T__'8866'_14]
v0
  = (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
      Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
      (Text
"[" :: Data.Text.Text)
      ((Text -> Text -> Text) -> AgdaAny -> Text -> AgdaAny
forall a b. a -> b
coe
         Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
         (([T__'8866'_14] -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14] -> Text
du_uglyList''_106 ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v0)) (Text
"]" :: Data.Text.Text))
-- Untyped.uglyList'
d_uglyList''_106 ::
  () -> [T__'8866'_14] -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_uglyList''_106 :: () -> [T__'8866'_14] -> Text
d_uglyList''_106 ~()
v0 [T__'8866'_14]
v1 = [T__'8866'_14] -> Text
du_uglyList''_106 [T__'8866'_14]
v1
du_uglyList''_106 ::
  [T__'8866'_14] -> MAlonzo.Code.Agda.Builtin.String.T_String_6
du_uglyList''_106 :: [T__'8866'_14] -> Text
du_uglyList''_106 [T__'8866'_14]
v0
  = case [T__'8866'_14] -> [AgdaAny]
forall a b. a -> b
coe [T__'8866'_14]
v0 of
      [] -> Text -> Text
forall a b. a -> b
coe (Text
"" :: Data.Text.Text)
      (:) AgdaAny
v1 [AgdaAny]
v2
        -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             ((T__'8866'_14 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> Text
du_ugly_110 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
             ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                (Text
" , " :: Data.Text.Text) (([T__'8866'_14] -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14] -> Text
du_uglyList''_106 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)))
      [AgdaAny]
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.ugly
d_ugly_110 ::
  () -> T__'8866'_14 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_ugly_110 :: () -> T__'8866'_14 -> Text
d_ugly_110 ~()
v0 T__'8866'_14
v1 = T__'8866'_14 -> Text
du_ugly_110 T__'8866'_14
v1
du_ugly_110 ::
  T__'8866'_14 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
du_ugly_110 :: T__'8866'_14 -> Text
du_ugly_110 T__'8866'_14
v0
  = case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v0 of
      C_'96'_18 AgdaAny
v1 -> Text -> Text
forall a b. a -> b
coe (Text
"(` var )" :: Data.Text.Text)
      C_ƛ_20 T__'8866'_14
v1
        -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"(\411 " :: Data.Text.Text)
             ((Text -> Text -> Text) -> AgdaAny -> Text -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                ((T__'8866'_14 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> Text
du_ugly_110 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v1)) (Text
")" :: Data.Text.Text))
      C__'183'__22 T__'8866'_14
v1 T__'8866'_14
v2
        -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"( " :: Data.Text.Text)
             ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                ((T__'8866'_14 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> Text
du_ugly_110 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v1))
                ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                   (Text
" \183 " :: Data.Text.Text)
                   ((Text -> Text -> Text) -> AgdaAny -> Text -> AgdaAny
forall a b. a -> b
coe
                      Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                      ((T__'8866'_14 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> Text
du_ugly_110 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2)) (Text
")" :: Data.Text.Text))))
      C_force_24 T__'8866'_14
v1
        -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"(force " :: Data.Text.Text)
             ((Text -> Text -> Text) -> AgdaAny -> Text -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                ((T__'8866'_14 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> Text
du_ugly_110 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v1)) (Text
")" :: Data.Text.Text))
      C_delay_26 T__'8866'_14
v1
        -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"(delay " :: Data.Text.Text)
             ((Text -> Text -> Text) -> AgdaAny -> Text -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                ((T__'8866'_14 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> Text
du_ugly_110 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v1)) (Text
")" :: Data.Text.Text))
      C_con_28 T_TmCon_198
v1
        -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"(con " :: Data.Text.Text)
             ((Text -> Text -> Text) -> Text -> Text -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                (T_TmCon_198 -> Text
d_uglyTmCon_68 (T_TmCon_198 -> T_TmCon_198
forall a b. a -> b
coe T_TmCon_198
v1)) (Text
")" :: Data.Text.Text))
      C_constr_34 Integer
v1 [T__'8866'_14]
v2
        -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"(constr " :: Data.Text.Text)
             ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                ((Integer -> Text) -> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 Integer
v1)
                ((Text -> Text -> Text) -> AgdaAny -> Text -> AgdaAny
forall a b. a -> b
coe
                   Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                   (([T__'8866'_14] -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14] -> Text
du_uglyList_102 ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2)) (Text
")" :: Data.Text.Text)))
      C_case_40 T__'8866'_14
v1 [T__'8866'_14]
v2
        -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"(case " :: Data.Text.Text)
             ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                ((T__'8866'_14 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> Text
du_ugly_110 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v1))
                ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                   (Text
" " :: Data.Text.Text)
                   ((Text -> Text -> Text) -> AgdaAny -> Text -> AgdaAny
forall a b. a -> b
coe
                      Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                      (([T__'8866'_14] -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14] -> Text
du_uglyList_102 ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2)) (Text
")" :: Data.Text.Text))))
      C_builtin_44 T_Builtin_2
v1
        -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"(builtin " :: Data.Text.Text)
             ((Text -> Text -> Text) -> Text -> Text -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                (T_Builtin_2 -> Text
d_uglyBuiltin_98 (T_Builtin_2 -> T_Builtin_2
forall a b. a -> b
coe T_Builtin_2
v1)) (Text
")" :: Data.Text.Text))
      T__'8866'_14
C_error_46 -> Text -> Text
forall a b. a -> b
coe (Text
"error" :: Data.Text.Text)
      T__'8866'_14
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.extG
d_extG_144 ::
  () -> (AgdaAny -> Integer) -> Maybe AgdaAny -> Integer
d_extG_144 :: () -> (AgdaAny -> Integer) -> Maybe AgdaAny -> Integer
d_extG_144 ~()
v0 AgdaAny -> Integer
v1 Maybe AgdaAny
v2 = (AgdaAny -> Integer) -> Maybe AgdaAny -> Integer
du_extG_144 AgdaAny -> Integer
v1 Maybe AgdaAny
v2
du_extG_144 :: (AgdaAny -> Integer) -> Maybe AgdaAny -> Integer
du_extG_144 :: (AgdaAny -> Integer) -> Maybe AgdaAny -> Integer
du_extG_144 AgdaAny -> Integer
v0 Maybe AgdaAny
v1
  = case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
      MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 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)) ((AgdaAny -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Integer
v0 AgdaAny
v2)
      Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      Maybe AgdaAny
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.extricateUList
d_extricateUList_154 ::
  () ->
  (AgdaAny -> Integer) ->
  [T__'8866'_14] ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.RawU.T_Untyped_146
d_extricateUList_154 :: ()
-> (AgdaAny -> Integer)
-> [T__'8866'_14]
-> T_List_382 T_Untyped_146
d_extricateUList_154 ~()
v0 AgdaAny -> Integer
v1 [T__'8866'_14]
v2 = (AgdaAny -> Integer) -> [T__'8866'_14] -> T_List_382 T_Untyped_146
du_extricateUList_154 AgdaAny -> Integer
v1 [T__'8866'_14]
v2
du_extricateUList_154 ::
  (AgdaAny -> Integer) ->
  [T__'8866'_14] ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.RawU.T_Untyped_146
du_extricateUList_154 :: (AgdaAny -> Integer) -> [T__'8866'_14] -> T_List_382 T_Untyped_146
du_extricateUList_154 AgdaAny -> Integer
v0 [T__'8866'_14]
v1
  = case [T__'8866'_14] -> [AgdaAny]
forall a b. a -> b
coe [T__'8866'_14]
v1 of
      [] -> [AgdaAny] -> T_List_382 T_Untyped_146
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Utils.C_'91''93'_386
      (:) AgdaAny
v2 [AgdaAny]
v3
        -> (AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> T_List_382 T_Untyped_146
forall a b. a -> b
coe
             AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
             (((AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146
du_extricateU_158 ((AgdaAny -> Integer) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Integer
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
             (((AgdaAny -> Integer)
 -> [T__'8866'_14] -> T_List_382 T_Untyped_146)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> Integer) -> [T__'8866'_14] -> T_List_382 T_Untyped_146
du_extricateUList_154 ((AgdaAny -> Integer) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Integer
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3))
      [AgdaAny]
_ -> T_List_382 T_Untyped_146
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.extricateU
d_extricateU_158 ::
  () ->
  (AgdaAny -> Integer) ->
  T__'8866'_14 -> MAlonzo.Code.RawU.T_Untyped_146
d_extricateU_158 :: () -> (AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146
d_extricateU_158 ~()
v0 AgdaAny -> Integer
v1 T__'8866'_14
v2 = (AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146
du_extricateU_158 AgdaAny -> Integer
v1 T__'8866'_14
v2
du_extricateU_158 ::
  (AgdaAny -> Integer) ->
  T__'8866'_14 -> MAlonzo.Code.RawU.T_Untyped_146
du_extricateU_158 :: (AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146
du_extricateU_158 AgdaAny -> Integer
v0 T__'8866'_14
v1
  = case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
      C_'96'_18 AgdaAny
v2 -> (Integer -> T_Untyped_146) -> AgdaAny -> T_Untyped_146
forall a b. a -> b
coe Integer -> T_Untyped_146
MAlonzo.Code.RawU.C_UVar_148 ((AgdaAny -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Integer
v0 AgdaAny
v2)
      C_ƛ_20 T__'8866'_14
v2
        -> (T_Untyped_146 -> T_Untyped_146) -> AgdaAny -> T_Untyped_146
forall a b. a -> b
coe
             T_Untyped_146 -> T_Untyped_146
MAlonzo.Code.RawU.C_ULambda_150
             (((AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146
du_extricateU_158 (((AgdaAny -> Integer) -> Maybe AgdaAny -> Integer)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> Integer) -> Maybe AgdaAny -> Integer
du_extG_144 ((AgdaAny -> Integer) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Integer
v0)) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
      C__'183'__22 T__'8866'_14
v2 T__'8866'_14
v3
        -> (T_Untyped_146 -> T_Untyped_146 -> T_Untyped_146)
-> AgdaAny -> AgdaAny -> T_Untyped_146
forall a b. a -> b
coe
             T_Untyped_146 -> T_Untyped_146 -> T_Untyped_146
MAlonzo.Code.RawU.C_UApp_152
             (((AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146
du_extricateU_158 ((AgdaAny -> Integer) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Integer
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
             (((AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146
du_extricateU_158 ((AgdaAny -> Integer) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Integer
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v3))
      C_force_24 T__'8866'_14
v2
        -> (T_Untyped_146 -> T_Untyped_146) -> AgdaAny -> T_Untyped_146
forall a b. a -> b
coe
             T_Untyped_146 -> T_Untyped_146
MAlonzo.Code.RawU.C_UForce_162
             (((AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146
du_extricateU_158 ((AgdaAny -> Integer) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Integer
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
      C_delay_26 T__'8866'_14
v2
        -> (T_Untyped_146 -> T_Untyped_146) -> AgdaAny -> T_Untyped_146
forall a b. a -> b
coe
             T_Untyped_146 -> T_Untyped_146
MAlonzo.Code.RawU.C_UDelay_160
             (((AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146
du_extricateU_158 ((AgdaAny -> Integer) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Integer
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
      C_con_28 T_TmCon_198
v2
        -> (Some (ValueOf DefaultUni) -> T_Untyped_146)
-> AgdaAny -> T_Untyped_146
forall a b. a -> b
coe
             Some (ValueOf DefaultUni) -> T_Untyped_146
MAlonzo.Code.RawU.C_UCon_154
             ((T_TmCon_198 -> Some (ValueOf DefaultUni)) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TmCon_198 -> Some (ValueOf DefaultUni)
MAlonzo.Code.RawU.d_tmCon2TagCon_316 (T_TmCon_198 -> AgdaAny
forall a b. a -> b
coe T_TmCon_198
v2))
      C_constr_34 Integer
v2 [T__'8866'_14]
v3
        -> case [T__'8866'_14] -> [AgdaAny]
forall a b. a -> b
coe [T__'8866'_14]
v3 of
             []
               -> (Integer -> T_List_382 T_Untyped_146 -> T_Untyped_146)
-> AgdaAny -> AgdaAny -> T_Untyped_146
forall a b. a -> b
coe
                    Integer -> T_List_382 T_Untyped_146 -> T_Untyped_146
MAlonzo.Code.RawU.C_UConstr_164 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
                    ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Utils.C_'91''93'_386)
             (:) AgdaAny
v4 [AgdaAny]
v5
               -> (Integer -> T_List_382 T_Untyped_146 -> T_Untyped_146)
-> AgdaAny -> AgdaAny -> T_Untyped_146
forall a b. a -> b
coe
                    Integer -> T_List_382 T_Untyped_146 -> T_Untyped_146
MAlonzo.Code.RawU.C_UConstr_164 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
                    ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
                       (((AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146
du_extricateU_158 ((AgdaAny -> Integer) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Integer
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
                       (((AgdaAny -> Integer)
 -> [T__'8866'_14] -> T_List_382 T_Untyped_146)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> Integer) -> [T__'8866'_14] -> T_List_382 T_Untyped_146
du_extricateUList_154 ((AgdaAny -> Integer) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Integer
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5)))
             [AgdaAny]
_ -> T_Untyped_146
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_case_40 T__'8866'_14
v2 [T__'8866'_14]
v3
        -> (T_Untyped_146 -> T_List_382 T_Untyped_146 -> T_Untyped_146)
-> AgdaAny -> AgdaAny -> T_Untyped_146
forall a b. a -> b
coe
             T_Untyped_146 -> T_List_382 T_Untyped_146 -> T_Untyped_146
MAlonzo.Code.RawU.C_UCase_166
             (((AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146
du_extricateU_158 ((AgdaAny -> Integer) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Integer
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
             (((AgdaAny -> Integer)
 -> [T__'8866'_14] -> T_List_382 T_Untyped_146)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> Integer) -> [T__'8866'_14] -> T_List_382 T_Untyped_146
du_extricateUList_154 ((AgdaAny -> Integer) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Integer
v0) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v3))
      C_builtin_44 T_Builtin_2
v2 -> (T_Builtin_2 -> T_Untyped_146) -> AgdaAny -> T_Untyped_146
forall a b. a -> b
coe T_Builtin_2 -> T_Untyped_146
MAlonzo.Code.RawU.C_UBuiltin_158 (T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v2)
      T__'8866'_14
C_error_46 -> T_Untyped_146 -> T_Untyped_146
forall a b. a -> b
coe T_Untyped_146
MAlonzo.Code.RawU.C_UError_156
      T__'8866'_14
_ -> T_Untyped_146
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.extricateU0
d_extricateU0_218 ::
  T__'8866'_14 -> MAlonzo.Code.RawU.T_Untyped_146
d_extricateU0_218 :: T__'8866'_14 -> T_Untyped_146
d_extricateU0_218 T__'8866'_14
v0 = ((AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146)
-> AgdaAny -> AgdaAny -> T_Untyped_146
forall a b. a -> b
coe (AgdaAny -> Integer) -> T__'8866'_14 -> T_Untyped_146
du_extricateU_158 AgdaAny
forall a. a
erased (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v0)
-- Untyped.extG'
d_extG''_224 ::
  () ->
  (Integer ->
   MAlonzo.Code.Utils.T_Either_6
     MAlonzo.Code.Scoped.T_ScopeError_576 AgdaAny) ->
  Integer ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_ScopeError_576 (Maybe AgdaAny)
d_extG''_224 :: ()
-> (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> Integer
-> T_Either_6 T_ScopeError_576 (Maybe AgdaAny)
d_extG''_224 ~()
v0 Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v1 Integer
v2 = (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> Integer -> T_Either_6 T_ScopeError_576 (Maybe AgdaAny)
du_extG''_224 Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v1 Integer
v2
du_extG''_224 ::
  (Integer ->
   MAlonzo.Code.Utils.T_Either_6
     MAlonzo.Code.Scoped.T_ScopeError_576 AgdaAny) ->
  Integer ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_ScopeError_576 (Maybe AgdaAny)
du_extG''_224 :: (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> Integer -> T_Either_6 T_ScopeError_576 (Maybe AgdaAny)
du_extG''_224 Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> (AgdaAny -> Either AgdaAny AgdaAny)
-> AgdaAny -> T_Either_6 T_ScopeError_576 (Maybe AgdaAny)
forall a b. a -> b
coe
             AgdaAny -> Either AgdaAny AgdaAny
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
             (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> T_Either_6 T_ScopeError_576 (Maybe AgdaAny)
forall a b. a -> b
coe
             ((T_Monad_186 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Monad_186 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Utils.du_fmap_224
                (T_Monad_186 -> AgdaAny
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.du_EitherP_274)
                ((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) ((Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v0 Integer
v2))
-- Untyped.scopeCheckUList
d_scopeCheckUList_234 ::
  () ->
  (Integer ->
   MAlonzo.Code.Utils.T_Either_6
     MAlonzo.Code.Scoped.T_ScopeError_576 AgdaAny) ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.RawU.T_Untyped_146 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_ScopeError_576 [T__'8866'_14]
d_scopeCheckUList_234 :: ()
-> (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_List_382 T_Untyped_146
-> T_Either_6 T_ScopeError_576 [T__'8866'_14]
d_scopeCheckUList_234 ~()
v0 Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v1 T_List_382 T_Untyped_146
v2 = (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_List_382 T_Untyped_146
-> T_Either_6 T_ScopeError_576 [T__'8866'_14]
du_scopeCheckUList_234 Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v1 T_List_382 T_Untyped_146
v2
du_scopeCheckUList_234 ::
  (Integer ->
   MAlonzo.Code.Utils.T_Either_6
     MAlonzo.Code.Scoped.T_ScopeError_576 AgdaAny) ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.RawU.T_Untyped_146 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_ScopeError_576 [T__'8866'_14]
du_scopeCheckUList_234 :: (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_List_382 T_Untyped_146
-> T_Either_6 T_ScopeError_576 [T__'8866'_14]
du_scopeCheckUList_234 Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v0 T_List_382 T_Untyped_146
v1
  = case T_List_382 T_Untyped_146 -> [AgdaAny]
forall a b. a -> b
coe T_List_382 T_Untyped_146
v1 of
      [AgdaAny]
MAlonzo.Code.Utils.C_'91''93'_386
        -> (AgdaAny -> Either AgdaAny AgdaAny)
-> AgdaAny -> T_Either_6 T_ScopeError_576 [T__'8866'_14]
forall a b. a -> b
coe
             AgdaAny -> Either AgdaAny AgdaAny
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
             ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
      MAlonzo.Code.Utils.C__'8759'__388 AgdaAny
v2 [AgdaAny]
v3
        -> (Either AgdaAny AgdaAny
 -> (AgdaAny -> Either AgdaAny AgdaAny) -> Either AgdaAny AgdaAny)
-> AgdaAny -> AgdaAny -> T_Either_6 T_ScopeError_576 [T__'8866'_14]
forall a b. a -> b
coe
             Either AgdaAny AgdaAny
-> (AgdaAny -> Either AgdaAny AgdaAny) -> Either AgdaAny AgdaAny
MAlonzo.Code.Utils.du_eitherBind_42
             (((Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
 -> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14
du_scopeCheckU_238 ((Integer -> T_Either_6 T_ScopeError_576 AgdaAny) -> AgdaAny
forall a b. a -> b
coe Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
             ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                (\ AgdaAny
v4 ->
                   (Either AgdaAny AgdaAny
 -> (AgdaAny -> Either AgdaAny AgdaAny) -> Either AgdaAny AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     Either AgdaAny AgdaAny
-> (AgdaAny -> Either AgdaAny AgdaAny) -> Either AgdaAny AgdaAny
MAlonzo.Code.Utils.du_eitherBind_42
                     (((Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
 -> T_List_382 T_Untyped_146
 -> T_Either_6 T_ScopeError_576 [T__'8866'_14])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_List_382 T_Untyped_146
-> T_Either_6 T_ScopeError_576 [T__'8866'_14]
du_scopeCheckUList_234 ((Integer -> T_Either_6 T_ScopeError_576 AgdaAny) -> AgdaAny
forall a b. a -> b
coe Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3))
                     ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                        (\ AgdaAny
v5 ->
                           (AgdaAny -> Either AgdaAny AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             AgdaAny -> Either AgdaAny AgdaAny
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                             ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))))))
      [AgdaAny]
_ -> T_Either_6 T_ScopeError_576 [T__'8866'_14]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.scopeCheckU
d_scopeCheckU_238 ::
  () ->
  (Integer ->
   MAlonzo.Code.Utils.T_Either_6
     MAlonzo.Code.Scoped.T_ScopeError_576 AgdaAny) ->
  MAlonzo.Code.RawU.T_Untyped_146 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_ScopeError_576 T__'8866'_14
d_scopeCheckU_238 :: ()
-> (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_Untyped_146
-> T_Either_6 T_ScopeError_576 T__'8866'_14
d_scopeCheckU_238 ~()
v0 Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v1 T_Untyped_146
v2 = (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14
du_scopeCheckU_238 Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v1 T_Untyped_146
v2
du_scopeCheckU_238 ::
  (Integer ->
   MAlonzo.Code.Utils.T_Either_6
     MAlonzo.Code.Scoped.T_ScopeError_576 AgdaAny) ->
  MAlonzo.Code.RawU.T_Untyped_146 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_ScopeError_576 T__'8866'_14
du_scopeCheckU_238 :: (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14
du_scopeCheckU_238 Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v0 T_Untyped_146
v1
  = case T_Untyped_146 -> T_Untyped_146
forall a b. a -> b
coe T_Untyped_146
v1 of
      MAlonzo.Code.RawU.C_UVar_148 Integer
v2
        -> (T_Monad_186 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Either_6 T_ScopeError_576 T__'8866'_14
forall a b. a -> b
coe
             T_Monad_186 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Utils.du_fmap_224
             (T_Monad_186 -> AgdaAny
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.du_EitherP_274) ((AgdaAny -> T__'8866'_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
C_'96'_18) ((Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v0 Integer
v2)
      MAlonzo.Code.RawU.C_ULambda_150 T_Untyped_146
v2
        -> (T_Monad_186 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Either_6 T_ScopeError_576 T__'8866'_14
forall a b. a -> b
coe
             T_Monad_186 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Utils.du_fmap_224
             (T_Monad_186 -> AgdaAny
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.du_EitherP_274) ((T__'8866'_14 -> T__'8866'_14) -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14
C_ƛ_20)
             (((Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
 -> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14
du_scopeCheckU_238 (((Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
 -> Integer -> T_Either_6 T_ScopeError_576 (Maybe AgdaAny))
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> Integer -> T_Either_6 T_ScopeError_576 (Maybe AgdaAny)
du_extG''_224 ((Integer -> T_Either_6 T_ScopeError_576 AgdaAny) -> AgdaAny
forall a b. a -> b
coe Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v0)) (T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_Untyped_146
v2))
      MAlonzo.Code.RawU.C_UApp_152 T_Untyped_146
v2 T_Untyped_146
v3
        -> (Either AgdaAny AgdaAny
 -> (AgdaAny -> Either AgdaAny AgdaAny) -> Either AgdaAny AgdaAny)
-> AgdaAny -> AgdaAny -> T_Either_6 T_ScopeError_576 T__'8866'_14
forall a b. a -> b
coe
             Either AgdaAny AgdaAny
-> (AgdaAny -> Either AgdaAny AgdaAny) -> Either AgdaAny AgdaAny
MAlonzo.Code.Utils.du_eitherBind_42
             (((Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
 -> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14
du_scopeCheckU_238 ((Integer -> T_Either_6 T_ScopeError_576 AgdaAny) -> AgdaAny
forall a b. a -> b
coe Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v0) (T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_Untyped_146
v2))
             ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                (\ AgdaAny
v4 ->
                   (Either AgdaAny AgdaAny
 -> (AgdaAny -> Either AgdaAny AgdaAny) -> Either AgdaAny AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     Either AgdaAny AgdaAny
-> (AgdaAny -> Either AgdaAny AgdaAny) -> Either AgdaAny AgdaAny
MAlonzo.Code.Utils.du_eitherBind_42
                     (((Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
 -> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14
du_scopeCheckU_238 ((Integer -> T_Either_6 T_ScopeError_576 AgdaAny) -> AgdaAny
forall a b. a -> b
coe Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v0) (T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_Untyped_146
v3))
                     ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                        (\ AgdaAny
v5 ->
                           (AgdaAny -> Either AgdaAny AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             AgdaAny -> Either AgdaAny AgdaAny
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                             ((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
C__'183'__22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))))))
      MAlonzo.Code.RawU.C_UCon_154 Some (ValueOf DefaultUni)
v2
        -> (AgdaAny -> Either AgdaAny AgdaAny)
-> AgdaAny -> T_Either_6 T_ScopeError_576 T__'8866'_14
forall a b. a -> b
coe
             AgdaAny -> Either AgdaAny AgdaAny
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
             ((T_TmCon_198 -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TmCon_198 -> T__'8866'_14
C_con_28 ((Some (ValueOf DefaultUni) -> T_TmCon_198) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Some (ValueOf DefaultUni) -> T_TmCon_198
MAlonzo.Code.RawU.d_tagCon2TmCon_226 (Some (ValueOf DefaultUni) -> AgdaAny
forall a b. a -> b
coe Some (ValueOf DefaultUni)
v2)))
      T_Untyped_146
MAlonzo.Code.RawU.C_UError_156
        -> (AgdaAny -> Either AgdaAny AgdaAny)
-> AgdaAny -> T_Either_6 T_ScopeError_576 T__'8866'_14
forall a b. a -> b
coe AgdaAny -> Either AgdaAny AgdaAny
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
C_error_46)
      MAlonzo.Code.RawU.C_UBuiltin_158 T_Builtin_2
v2
        -> (AgdaAny -> Either AgdaAny AgdaAny)
-> AgdaAny -> T_Either_6 T_ScopeError_576 T__'8866'_14
forall a b. a -> b
coe
             AgdaAny -> Either AgdaAny AgdaAny
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 ((T_Builtin_2 -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Builtin_2 -> T__'8866'_14
C_builtin_44 (T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v2))
      MAlonzo.Code.RawU.C_UDelay_160 T_Untyped_146
v2
        -> (T_Monad_186 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Either_6 T_ScopeError_576 T__'8866'_14
forall a b. a -> b
coe
             T_Monad_186 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Utils.du_fmap_224
             (T_Monad_186 -> AgdaAny
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.du_EitherP_274) ((T__'8866'_14 -> T__'8866'_14) -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14
C_delay_26)
             (((Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
 -> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14
du_scopeCheckU_238 ((Integer -> T_Either_6 T_ScopeError_576 AgdaAny) -> AgdaAny
forall a b. a -> b
coe Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v0) (T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_Untyped_146
v2))
      MAlonzo.Code.RawU.C_UForce_162 T_Untyped_146
v2
        -> (T_Monad_186 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Either_6 T_ScopeError_576 T__'8866'_14
forall a b. a -> b
coe
             T_Monad_186 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Utils.du_fmap_224
             (T_Monad_186 -> AgdaAny
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.du_EitherP_274) ((T__'8866'_14 -> T__'8866'_14) -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14
C_force_24)
             (((Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
 -> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14
du_scopeCheckU_238 ((Integer -> T_Either_6 T_ScopeError_576 AgdaAny) -> AgdaAny
forall a b. a -> b
coe Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v0) (T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_Untyped_146
v2))
      MAlonzo.Code.RawU.C_UConstr_164 Integer
v2 T_List_382 T_Untyped_146
v3
        -> (T_Monad_186 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Either_6 T_ScopeError_576 T__'8866'_14
forall a b. a -> b
coe
             T_Monad_186 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Utils.du_fmap_224
             (T_Monad_186 -> AgdaAny
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.du_EitherP_274) ((Integer -> [T__'8866'_14] -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> [T__'8866'_14] -> T__'8866'_14
C_constr_34 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2))
             (((Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
 -> T_List_382 T_Untyped_146
 -> T_Either_6 T_ScopeError_576 [T__'8866'_14])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_List_382 T_Untyped_146
-> T_Either_6 T_ScopeError_576 [T__'8866'_14]
du_scopeCheckUList_234 ((Integer -> T_Either_6 T_ScopeError_576 AgdaAny) -> AgdaAny
forall a b. a -> b
coe Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v0) (T_List_382 T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_List_382 T_Untyped_146
v3))
      MAlonzo.Code.RawU.C_UCase_166 T_Untyped_146
v2 T_List_382 T_Untyped_146
v3
        -> (Either AgdaAny AgdaAny
 -> (AgdaAny -> Either AgdaAny AgdaAny) -> Either AgdaAny AgdaAny)
-> AgdaAny -> AgdaAny -> T_Either_6 T_ScopeError_576 T__'8866'_14
forall a b. a -> b
coe
             Either AgdaAny AgdaAny
-> (AgdaAny -> Either AgdaAny AgdaAny) -> Either AgdaAny AgdaAny
MAlonzo.Code.Utils.du_eitherBind_42
             (((Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
 -> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14
du_scopeCheckU_238 ((Integer -> T_Either_6 T_ScopeError_576 AgdaAny) -> AgdaAny
forall a b. a -> b
coe Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v0) (T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_Untyped_146
v2))
             ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                (\ AgdaAny
v4 ->
                   (Either AgdaAny AgdaAny
 -> (AgdaAny -> Either AgdaAny AgdaAny) -> Either AgdaAny AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     Either AgdaAny AgdaAny
-> (AgdaAny -> Either AgdaAny AgdaAny) -> Either AgdaAny AgdaAny
MAlonzo.Code.Utils.du_eitherBind_42
                     (((Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
 -> T_List_382 T_Untyped_146
 -> T_Either_6 T_ScopeError_576 [T__'8866'_14])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_List_382 T_Untyped_146
-> T_Either_6 T_ScopeError_576 [T__'8866'_14]
du_scopeCheckUList_234 ((Integer -> T_Either_6 T_ScopeError_576 AgdaAny) -> AgdaAny
forall a b. a -> b
coe Integer -> T_Either_6 T_ScopeError_576 AgdaAny
v0) (T_List_382 T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_List_382 T_Untyped_146
v3))
                     ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                        (\ AgdaAny
v5 ->
                           (AgdaAny -> Either AgdaAny AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             AgdaAny -> Either AgdaAny AgdaAny
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                             ((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
C_case_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))))))
      T_Untyped_146
_ -> T_Either_6 T_ScopeError_576 T__'8866'_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Untyped.scopeCheckU0
d_scopeCheckU0_304 ::
  MAlonzo.Code.RawU.T_Untyped_146 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_ScopeError_576 T__'8866'_14
d_scopeCheckU0_304 :: T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14
d_scopeCheckU0_304 T_Untyped_146
v0
  = ((Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
 -> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14)
-> AgdaAny -> AgdaAny -> T_Either_6 T_ScopeError_576 T__'8866'_14
forall a b. a -> b
coe
      (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14
du_scopeCheckU_238
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 ->
            (AgdaAny -> Either AgdaAny AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              AgdaAny -> Either AgdaAny AgdaAny
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
              (T_ScopeError_576 -> AgdaAny
forall a b. a -> b
coe T_ScopeError_576
MAlonzo.Code.Scoped.C_deBError_578)))
      (T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_Untyped_146
v0)
-- Untyped.decUTm
d_decUTm_314 ::
  MAlonzo.Code.RawU.T_Untyped_146 ->
  MAlonzo.Code.RawU.T_Untyped_146 -> Bool
d_decUTm_314 :: T_Untyped_146 -> T_Untyped_146 -> Bool
d_decUTm_314 T_Untyped_146
v0 T_Untyped_146
v1
  = let v2 :: b
v2 = Bool -> b
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8 in
    AgdaAny -> Bool
forall a b. a -> b
coe
      (case T_Untyped_146 -> T_Untyped_146
forall a b. a -> b
coe T_Untyped_146
v0 of
         MAlonzo.Code.RawU.C_UVar_148 Integer
v3
           -> case T_Untyped_146 -> T_Untyped_146
forall a b. a -> b
coe T_Untyped_146
v1 of
                MAlonzo.Code.RawU.C_UVar_148 Integer
v4
                  -> (T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Dec_20 -> Bool
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_does_28
                       ((Integer -> Integer -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3))
                T_Untyped_146
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2
         MAlonzo.Code.RawU.C_ULambda_150 T_Untyped_146
v3
           -> case T_Untyped_146 -> T_Untyped_146
forall a b. a -> b
coe T_Untyped_146
v1 of
                MAlonzo.Code.RawU.C_ULambda_150 T_Untyped_146
v4
                  -> (T_Untyped_146 -> T_Untyped_146 -> Bool)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Untyped_146 -> T_Untyped_146 -> Bool
d_decUTm_314 (T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_Untyped_146
v3) (T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_Untyped_146
v4)
                T_Untyped_146
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2
         MAlonzo.Code.RawU.C_UApp_152 T_Untyped_146
v3 T_Untyped_146
v4
           -> case T_Untyped_146 -> T_Untyped_146
forall a b. a -> b
coe T_Untyped_146
v1 of
                MAlonzo.Code.RawU.C_UApp_152 T_Untyped_146
v5 T_Untyped_146
v6
                  -> (Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
                       ((T_Untyped_146 -> T_Untyped_146 -> Bool)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Untyped_146 -> T_Untyped_146 -> Bool
d_decUTm_314 (T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_Untyped_146
v3) (T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_Untyped_146
v5))
                       ((T_Untyped_146 -> T_Untyped_146 -> Bool)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Untyped_146 -> T_Untyped_146 -> Bool
d_decUTm_314 (T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_Untyped_146
v4) (T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_Untyped_146
v6))
                T_Untyped_146
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2
         MAlonzo.Code.RawU.C_UCon_154 Some (ValueOf DefaultUni)
v3
           -> case T_Untyped_146 -> T_Untyped_146
forall a b. a -> b
coe T_Untyped_146
v1 of
                MAlonzo.Code.RawU.C_UCon_154 Some (ValueOf DefaultUni)
v4
                  -> (Some (ValueOf DefaultUni) -> Some (ValueOf DefaultUni) -> Bool)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Some (ValueOf DefaultUni) -> Some (ValueOf DefaultUni) -> Bool
MAlonzo.Code.RawU.d_decTagCon_136 (Some (ValueOf DefaultUni) -> AgdaAny
forall a b. a -> b
coe Some (ValueOf DefaultUni)
v3) (Some (ValueOf DefaultUni) -> AgdaAny
forall a b. a -> b
coe Some (ValueOf DefaultUni)
v4)
                T_Untyped_146
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2
         T_Untyped_146
MAlonzo.Code.RawU.C_UError_156
           -> case T_Untyped_146 -> T_Untyped_146
forall a b. a -> b
coe T_Untyped_146
v1 of
                T_Untyped_146
MAlonzo.Code.RawU.C_UError_156
                  -> Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
                T_Untyped_146
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2
         MAlonzo.Code.RawU.C_UBuiltin_158 T_Builtin_2
v3
           -> case T_Untyped_146 -> T_Untyped_146
forall a b. a -> b
coe T_Untyped_146
v1 of
                MAlonzo.Code.RawU.C_UBuiltin_158 T_Builtin_2
v4
                  -> (T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Dec_20 -> Bool
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_does_28
                       ((T_Builtin_2 -> T_Builtin_2 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Builtin_2 -> T_Builtin_2 -> T_Dec_20
MAlonzo.Code.Builtin.d_decBuiltin_398 (T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v3) (T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v4))
                T_Untyped_146
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2
         MAlonzo.Code.RawU.C_UDelay_160 T_Untyped_146
v3
           -> case T_Untyped_146 -> T_Untyped_146
forall a b. a -> b
coe T_Untyped_146
v1 of
                MAlonzo.Code.RawU.C_UDelay_160 T_Untyped_146
v4
                  -> (T_Untyped_146 -> T_Untyped_146 -> Bool)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Untyped_146 -> T_Untyped_146 -> Bool
d_decUTm_314 (T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_Untyped_146
v3) (T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_Untyped_146
v4)
                T_Untyped_146
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2
         MAlonzo.Code.RawU.C_UForce_162 T_Untyped_146
v3
           -> case T_Untyped_146 -> T_Untyped_146
forall a b. a -> b
coe T_Untyped_146
v1 of
                MAlonzo.Code.RawU.C_UForce_162 T_Untyped_146
v4
                  -> (T_Untyped_146 -> T_Untyped_146 -> Bool)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Untyped_146 -> T_Untyped_146 -> Bool
d_decUTm_314 (T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_Untyped_146
v3) (T_Untyped_146 -> AgdaAny
forall a b. a -> b
coe T_Untyped_146
v4)
                T_Untyped_146
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2
         T_Untyped_146
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2)
-- Untyped.buildDebruijnEncoding
d_buildDebruijnEncoding_350 ::
  () ->
  Integer ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_ScopeError_576 (Maybe AgdaAny)
d_buildDebruijnEncoding_350 :: () -> Integer -> T_Either_6 T_ScopeError_576 (Maybe AgdaAny)
d_buildDebruijnEncoding_350 ~()
v0 Integer
v1
  = Integer -> T_Either_6 T_ScopeError_576 (Maybe AgdaAny)
du_buildDebruijnEncoding_350 Integer
v1
du_buildDebruijnEncoding_350 ::
  Integer ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_ScopeError_576 (Maybe AgdaAny)
du_buildDebruijnEncoding_350 :: Integer -> T_Either_6 T_ScopeError_576 (Maybe AgdaAny)
du_buildDebruijnEncoding_350 Integer
v0
  = ((Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
 -> Integer -> T_Either_6 T_ScopeError_576 (Maybe AgdaAny))
-> AgdaAny
-> AgdaAny
-> T_Either_6 T_ScopeError_576 (Maybe AgdaAny)
forall a b. a -> b
coe
      (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> Integer -> T_Either_6 T_ScopeError_576 (Maybe AgdaAny)
du_extG''_224
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 ->
            (AgdaAny -> Either AgdaAny AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              AgdaAny -> Either AgdaAny AgdaAny
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
              (T_ScopeError_576 -> AgdaAny
forall a b. a -> b
coe T_ScopeError_576
MAlonzo.Code.Scoped.C_deBError_578)))
      (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0)
-- Untyped.toWellScoped
d_toWellScoped_358 ::
  () ->
  MAlonzo.Code.RawU.T_Untyped_146 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_ScopeError_576 T__'8866'_14
d_toWellScoped_358 :: () -> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14
d_toWellScoped_358 ~()
v0 = T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14
du_toWellScoped_358
du_toWellScoped_358 ::
  MAlonzo.Code.RawU.T_Untyped_146 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_ScopeError_576 T__'8866'_14
du_toWellScoped_358 :: T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14
du_toWellScoped_358
  = ((Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
 -> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14)
-> AgdaAny
-> T_Untyped_146
-> T_Either_6 T_ScopeError_576 T__'8866'_14
forall a b. a -> b
coe (Integer -> T_Either_6 T_ScopeError_576 AgdaAny)
-> T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14
du_scopeCheckU_238 ((Integer -> T_Either_6 T_ScopeError_576 (Maybe AgdaAny)) -> AgdaAny
forall a b. a -> b
coe Integer -> T_Either_6 T_ScopeError_576 (Maybe AgdaAny)
du_buildDebruijnEncoding_350)