{-# 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.Evaluator.Term 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.Sigma
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Algorithmic
import qualified MAlonzo.Code.Algorithmic.CEK
import qualified MAlonzo.Code.Algorithmic.CK
import qualified MAlonzo.Code.Algorithmic.Evaluation
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Check
import qualified MAlonzo.Code.Cost
import qualified MAlonzo.Code.Cost.Model
import qualified MAlonzo.Code.Cost.Raw
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.Evaluator.Base
import qualified MAlonzo.Code.Raw
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Scoped
import qualified MAlonzo.Code.Scoped.Extrication
import qualified MAlonzo.Code.Type
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.Untyped.CEK
import qualified MAlonzo.Code.Untyped.CEKWithCost
import qualified MAlonzo.Code.Utils

import Data.Bifunctor
import Data.Functor
import Data.Either
import Control.Monad.Trans.Except
import Raw
import PlutusCore
import PlutusCore.DeBruijn
import qualified UntypedPlutusCore as U
import qualified UntypedPlutusCore.Parser as U
import qualified Untyped as U
-- Evaluator.Term.Term
type T_Term_14 =
  PlutusCore.Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
d_Term_14 :: a
d_Term_14
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Term.Term"
-- Evaluator.Term.Type
type T_Type_16 = PlutusCore.Type NamedTyDeBruijn DefaultUni ()
d_Type_16 :: a
d_Type_16
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Term.Type"
-- Evaluator.Term.TermN
type T_TermN_18 =
  PlutusCore.Term TyName Name DefaultUni DefaultFun PlutusCore.SrcSpan
d_TermN_18 :: a
d_TermN_18
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Term.TermN"
-- Evaluator.Term.TypeN
type T_TypeN_20 =
  PlutusCore.Type TyName DefaultUni PlutusCore.SrcSpan
d_TypeN_20 :: a
d_TypeN_20
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Term.TypeN"
-- Evaluator.Term.TermNU
type T_TermNU_22 =
  U.Term Name DefaultUni DefaultFun PlutusCore.SrcSpan
d_TermNU_22 :: a
d_TermNU_22
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Term.TermNU"
-- Evaluator.Term.TermU
type T_TermU_24 = U.Term NamedDeBruijn DefaultUni DefaultFun ()
d_TermU_24 :: a
d_TermU_24
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Term.TermU"
-- Evaluator.Term.parseTm
d_parseTm_26 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ParseError_4 T_TermN_18
d_parseTm_26 :: Text -> T_Either_6 T_ParseError_4 T_TermN_18
d_parseTm_26 = QuoteT (Either T_ParseError_4) T_TermN_18
-> T_Either_6 T_ParseError_4 T_TermN_18
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT (QuoteT (Either T_ParseError_4) T_TermN_18
 -> T_Either_6 T_ParseError_4 T_TermN_18)
-> (Text -> QuoteT (Either T_ParseError_4) T_TermN_18)
-> Text
-> T_Either_6 T_ParseError_4 T_TermN_18
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> QuoteT (Either T_ParseError_4) T_TermN_18
forall e (m :: * -> *).
(AsParserErrorBundle e, MonadError e m, MonadQuote m) =>
Text -> m T_TermN_18
parseTerm
-- Evaluator.Term.parseTmU
d_parseTmU_28 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ParseError_4 T_TermNU_22
d_parseTmU_28 :: Text -> T_Either_6 T_ParseError_4 T_TermNU_22
d_parseTmU_28 = QuoteT (Either T_ParseError_4) T_TermNU_22
-> T_Either_6 T_ParseError_4 T_TermNU_22
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT (QuoteT (Either T_ParseError_4) T_TermNU_22
 -> T_Either_6 T_ParseError_4 T_TermNU_22)
-> (Text -> QuoteT (Either T_ParseError_4) T_TermNU_22)
-> Text
-> T_Either_6 T_ParseError_4 T_TermNU_22
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> QuoteT (Either T_ParseError_4) T_TermNU_22
forall e (m :: * -> *).
(AsParserErrorBundle e, MonadError e m, MonadQuote m) =>
Text -> m T_TermNU_22
U.parseTerm
-- Evaluator.Term.parseTy
d_parseTy_30 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ParseError_4 T_TypeN_20
d_parseTy_30 :: Text -> T_Either_6 T_ParseError_4 T_TypeN_20
d_parseTy_30 = QuoteT (Either T_ParseError_4) T_TypeN_20
-> T_Either_6 T_ParseError_4 T_TypeN_20
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT (QuoteT (Either T_ParseError_4) T_TypeN_20
 -> T_Either_6 T_ParseError_4 T_TypeN_20)
-> (Text -> QuoteT (Either T_ParseError_4) T_TypeN_20)
-> Text
-> T_Either_6 T_ParseError_4 T_TypeN_20
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> QuoteT (Either T_ParseError_4) T_TypeN_20
forall e (m :: * -> *).
(AsParserErrorBundle e, MonadError e m, MonadQuote m) =>
Text -> m T_TypeN_20
parseType
-- Evaluator.Term.deBruijnifyTm
d_deBruijnifyTm_32 ::
  T_TermN_18 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_FreeVariableError_574 T_Term_14
d_deBruijnifyTm_32 :: T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14
d_deBruijnifyTm_32 = (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan
 -> T_Term_14)
-> Either
     FreeVariableError
     (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> T_Either_6 FreeVariableError T_Term_14
forall b c a. (b -> c) -> Either a b -> Either a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan
-> T_Term_14
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Either
   FreeVariableError
   (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
 -> T_Either_6 FreeVariableError T_Term_14)
-> (T_TermN_18
    -> Either
         FreeVariableError
         (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan))
-> T_TermN_18
-> T_Either_6 FreeVariableError T_Term_14
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Except
  FreeVariableError
  (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> Either
     FreeVariableError
     (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
forall e a. Except e a -> Either e a
runExcept (Except
   FreeVariableError
   (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
 -> Either
      FreeVariableError
      (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan))
-> (T_TermN_18
    -> Except
         FreeVariableError
         (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan))
-> T_TermN_18
-> Either
     FreeVariableError
     (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T_TermN_18
-> Except
     FreeVariableError
     (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
forall e (m :: * -> *) (uni :: * -> *) fun ann.
(AsFreeVariableError e, MonadError e m) =>
Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
deBruijnTerm
-- Evaluator.Term.deBruijnifyTy
d_deBruijnifyTy_34 ::
  T_TypeN_20 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_FreeVariableError_574 T_Type_16
d_deBruijnifyTy_34 :: T_TypeN_20 -> T_Either_6 FreeVariableError T_Type_16
d_deBruijnifyTy_34 = (Type NamedTyDeBruijn DefaultUni SrcSpan -> T_Type_16)
-> Either
     FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan)
-> T_Either_6 FreeVariableError T_Type_16
forall b c a. (b -> c) -> Either a b -> Either a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Type NamedTyDeBruijn DefaultUni SrcSpan -> T_Type_16
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Either FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan)
 -> T_Either_6 FreeVariableError T_Type_16)
-> (T_TypeN_20
    -> Either
         FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan))
-> T_TypeN_20
-> T_Either_6 FreeVariableError T_Type_16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Except FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan)
-> Either
     FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan)
forall e a. Except e a -> Either e a
runExcept (Except FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan)
 -> Either
      FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan))
-> (T_TypeN_20
    -> Except
         FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan))
-> T_TypeN_20
-> Either
     FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T_TypeN_20
-> Except
     FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan)
forall e (m :: * -> *) (uni :: * -> *) ann.
(AsFreeVariableError e, MonadError e m) =>
Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
deBruijnTy
-- Evaluator.Term.deBruijnifyTmU
d_deBruijnifyTmU_36 ::
  T_TermNU_22 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_FreeVariableError_574 T_TermU_24
d_deBruijnifyTmU_36 :: T_TermNU_22 -> T_Either_6 FreeVariableError T_TermU_24
d_deBruijnifyTmU_36 = (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan -> T_TermU_24)
-> Either
     FreeVariableError
     (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> T_Either_6 FreeVariableError T_TermU_24
forall b c a. (b -> c) -> Either a b -> Either a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Term NamedDeBruijn DefaultUni DefaultFun SrcSpan -> T_TermU_24
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Either
   FreeVariableError
   (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
 -> T_Either_6 FreeVariableError T_TermU_24)
-> (T_TermNU_22
    -> Either
         FreeVariableError
         (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan))
-> T_TermNU_22
-> T_Either_6 FreeVariableError T_TermU_24
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Except
  FreeVariableError
  (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> Either
     FreeVariableError
     (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
forall e a. Except e a -> Either e a
runExcept (Except
   FreeVariableError
   (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
 -> Either
      FreeVariableError
      (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan))
-> (T_TermNU_22
    -> Except
         FreeVariableError
         (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan))
-> T_TermNU_22
-> Either
     FreeVariableError
     (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T_TermNU_22
-> Except
     FreeVariableError
     (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
forall e (m :: * -> *) (uni :: * -> *) fun ann.
(AsFreeVariableError e, MonadError e m) =>
Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
U.deBruijnTerm
-- Evaluator.Term.convTm
d_convTm_38 :: T_Term_14 -> MAlonzo.Code.Raw.T_RawTm_30
d_convTm_38 :: T_Term_14 -> T_RawTm_30
d_convTm_38 = T_Term_14 -> T_RawTm_30
forall a.
Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
-> T_RawTm_30
conv
-- Evaluator.Term.unconvTm
d_unconvTm_40 :: MAlonzo.Code.Raw.T_RawTm_30 -> T_Term_14
d_unconvTm_40 :: T_RawTm_30 -> T_Term_14
d_unconvTm_40 = Int -> T_RawTm_30 -> T_Term_14
unconv Int
0
-- Evaluator.Term.convTy
d_convTy_42 :: T_Type_16 -> MAlonzo.Code.Raw.T_RawTy_2
d_convTy_42 :: T_Type_16 -> T_RawTy_2
d_convTy_42 = T_Type_16 -> T_RawTy_2
forall a. Type NamedTyDeBruijn DefaultUni a -> T_RawTy_2
convT
-- Evaluator.Term.unconvTy
d_unconvTy_44 :: MAlonzo.Code.Raw.T_RawTy_2 -> T_Type_16
d_unconvTy_44 :: T_RawTy_2 -> T_Type_16
d_unconvTy_44 = Int -> T_RawTy_2 -> T_Type_16
unconvT Int
0
-- Evaluator.Term.convTmU
d_convTmU_46 :: T_TermU_24 -> MAlonzo.Code.RawU.T_Untyped_146
d_convTmU_46 :: T_TermU_24 -> T_Untyped_146
d_convTmU_46 = T_TermU_24 -> T_Untyped_146
forall a.
Term NamedDeBruijn DefaultUni DefaultFun a -> T_Untyped_146
U.conv
-- Evaluator.Term.unconvTmU
d_unconvTmU_48 :: MAlonzo.Code.RawU.T_Untyped_146 -> T_TermU_24
d_unconvTmU_48 :: T_Untyped_146 -> T_TermU_24
d_unconvTmU_48 = Int -> T_Untyped_146 -> T_TermU_24
U.uconv Int
0
-- Evaluator.Term.checkKindX
checkKindAgda ::
  T_Type_16 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
checkKindAgda :: T_Type_16 -> T_Kind_476 -> T_Either_6 T_ERROR_12 ()
checkKindAgda = (T_Type_16 -> T_Kind_476 -> T_Either_6 T_ERROR_12 ())
-> T_Type_16 -> T_Kind_476 -> T_Either_6 T_ERROR_12 ()
forall a b. a -> b
coe T_Type_16 -> T_Kind_476 -> T_Either_6 T_ERROR_12 ()
d_checkKindX_50
d_checkKindX_50 ::
  T_Type_16 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_checkKindX_50 :: T_Type_16 -> T_Kind_476 -> T_Either_6 T_ERROR_12 ()
d_checkKindX_50 T_Type_16
v0 T_Kind_476
v1
  = (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 ()
forall a b. a -> b
coe
      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
      (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
         ((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
         ((Integer -> T_RawTy_2 -> T_Either_6 ScopeError T_ScopedTy_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
            Integer -> T_RawTy_2 -> T_Either_6 ScopeError T_ScopedTy_14
MAlonzo.Code.Scoped.d_scopeCheckTy_616
            ((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
               T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Check.d_len'8902'_106
               (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
            ((Integer -> T_Weirdℕ_42 -> T_RawTy_2 -> T_RawTy_2)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> T_Weirdℕ_42 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Scoped.d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
               (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44) ((T_Type_16 -> T_RawTy_2) -> T_Type_16 -> Any
forall a b. a -> b
coe T_Type_16 -> T_RawTy_2
d_convTy_42 T_Type_16
v0))))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v2 ->
            (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
              T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
              (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                 (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                 ((Any -> Any) -> Any
forall a b. a -> b
coe
                    (\ Any
v3 ->
                       (Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                         Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_typeError_14
                         ((T_TypeError_12 -> Text) -> Any -> Any
forall a b. a -> b
coe T_TypeError_12 -> Text
MAlonzo.Code.Evaluator.Base.d_uglyTypeError_24 (Any -> Any
forall a b. a -> b
coe Any
v3))))
                 ((T_Ctx'8902'_2
 -> T_ScopedTy_14 -> T_Either_6 T_TypeError_12 T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
                    T_Ctx'8902'_2 -> T_ScopedTy_14 -> T_Either_6 T_TypeError_12 T_Σ_14
MAlonzo.Code.Check.d_inferKind_562
                    (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v2)))
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v3 ->
                    case Any -> T_Σ_14
forall a b. a -> b
coe Any
v3 of
                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v4 Any
v5
                        -> (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                             T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                             (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                                ((Any -> Any) -> Any
forall a b. a -> b
coe
                                   (\ Any
v6 ->
                                      (Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                                        Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_typeError_14
                                        ((T_TypeError_12 -> Text) -> Any -> Any
forall a b. a -> b
coe
                                           T_TypeError_12 -> Text
MAlonzo.Code.Evaluator.Base.d_uglyTypeError_24
                                           ((T_Kind_476 -> T_Kind_476 -> T_TypeError_12)
-> T_Kind_476 -> Any -> Any
forall a b. a -> b
coe T_Kind_476 -> T_Kind_476 -> T_TypeError_12
MAlonzo.Code.Check.C_kindMismatch_18 T_Kind_476
v1 Any
v4))))
                                ((T_Dec_20 -> T_Either_6 (Any -> T_Irrelevant_20) Any) -> Any -> Any
forall a b. a -> b
coe
                                   T_Dec_20 -> T_Either_6 (Any -> T_Irrelevant_20) Any
MAlonzo.Code.Utils.du_dec2Either_294
                                   ((T_Kind_476 -> T_Kind_476 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476 -> T_Kind_476 -> T_Dec_20
MAlonzo.Code.Check.d_decKind_138 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v1) (Any -> Any
forall a b. a -> b
coe Any
v4))))
                             ((Any -> Any) -> Any
forall a b. a -> b
coe
                                (\ Any
v6 ->
                                   (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                                     Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                                     (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)))
                      T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))))
-- Evaluator.Term.inferKind∅
inferKindAgda ::
  T_Type_16 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Utils.T_Kind_476
inferKindAgda :: T_Type_16 -> T_Either_6 T_ERROR_12 T_Kind_476
inferKindAgda = (T_Type_16 -> T_Either_6 T_ERROR_12 T_Kind_476)
-> T_Type_16 -> T_Either_6 T_ERROR_12 T_Kind_476
forall a b. a -> b
coe T_Type_16 -> T_Either_6 T_ERROR_12 T_Kind_476
d_inferKind'8709'_68
d_inferKind'8709'_68 ::
  T_Type_16 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Utils.T_Kind_476
d_inferKind'8709'_68 :: T_Type_16 -> T_Either_6 T_ERROR_12 T_Kind_476
d_inferKind'8709'_68 T_Type_16
v0
  = (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 T_Kind_476
forall a b. a -> b
coe
      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
      (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
         ((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
         ((Integer -> T_RawTy_2 -> T_Either_6 ScopeError T_ScopedTy_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
            Integer -> T_RawTy_2 -> T_Either_6 ScopeError T_ScopedTy_14
MAlonzo.Code.Scoped.d_scopeCheckTy_616
            ((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
               T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Check.d_len'8902'_106
               (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
            ((Integer -> T_Weirdℕ_42 -> T_RawTy_2 -> T_RawTy_2)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> T_Weirdℕ_42 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Scoped.d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
               (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44) ((T_Type_16 -> T_RawTy_2) -> T_Type_16 -> Any
forall a b. a -> b
coe T_Type_16 -> T_RawTy_2
d_convTy_42 T_Type_16
v0))))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 ->
            (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
              T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
              (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                 (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                 ((Any -> Any) -> Any
forall a b. a -> b
coe
                    (\ Any
v2 ->
                       (Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                         Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_typeError_14
                         ((T_TypeError_12 -> Text) -> Any -> Any
forall a b. a -> b
coe T_TypeError_12 -> Text
MAlonzo.Code.Evaluator.Base.d_uglyTypeError_24 (Any -> Any
forall a b. a -> b
coe Any
v2))))
                 ((T_Ctx'8902'_2
 -> T_ScopedTy_14 -> T_Either_6 T_TypeError_12 T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
                    T_Ctx'8902'_2 -> T_ScopedTy_14 -> T_Either_6 T_TypeError_12 T_Σ_14
MAlonzo.Code.Check.d_inferKind_562
                    (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v1)))
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v2 ->
                    case Any -> T_Σ_14
forall a b. a -> b
coe Any
v2 of
                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v3 Any
v4
                        -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 (Any -> Any
forall a b. a -> b
coe Any
v3)
                      T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))))
-- Evaluator.Term.normalizeType
normalizeTypeAgda ::
  T_Type_16 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Type_16
normalizeTypeAgda :: T_Type_16 -> T_Either_6 T_ERROR_12 T_Type_16
normalizeTypeAgda = (T_Type_16 -> T_Either_6 T_ERROR_12 T_Type_16)
-> T_Type_16 -> T_Either_6 T_ERROR_12 T_Type_16
forall a b. a -> b
coe T_Type_16 -> T_Either_6 T_ERROR_12 T_Type_16
d_normalizeType_80
d_normalizeType_80 ::
  T_Type_16 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Type_16
d_normalizeType_80 :: T_Type_16 -> T_Either_6 T_ERROR_12 T_Type_16
d_normalizeType_80 T_Type_16
v0
  = (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 T_Type_16
forall a b. a -> b
coe
      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
      (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
         ((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
         ((Integer -> T_RawTy_2 -> T_Either_6 ScopeError T_ScopedTy_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
            Integer -> T_RawTy_2 -> T_Either_6 ScopeError T_ScopedTy_14
MAlonzo.Code.Scoped.d_scopeCheckTy_616
            ((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
               T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Check.d_len'8902'_106
               (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
            ((Integer -> T_Weirdℕ_42 -> T_RawTy_2 -> T_RawTy_2)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> T_Weirdℕ_42 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Scoped.d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
               (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44) ((T_Type_16 -> T_RawTy_2) -> T_Type_16 -> Any
forall a b. a -> b
coe T_Type_16 -> T_RawTy_2
d_convTy_42 T_Type_16
v0))))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 ->
            (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
              T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
              (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                 (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                 ((Any -> Any) -> Any
forall a b. a -> b
coe
                    (\ Any
v2 ->
                       (Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                         Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_typeError_14
                         ((T_TypeError_12 -> Text) -> Any -> Any
forall a b. a -> b
coe T_TypeError_12 -> Text
MAlonzo.Code.Evaluator.Base.d_uglyTypeError_24 (Any -> Any
forall a b. a -> b
coe Any
v2))))
                 ((T_Ctx'8902'_2
 -> T_ScopedTy_14 -> T_Either_6 T_TypeError_12 T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
                    T_Ctx'8902'_2 -> T_ScopedTy_14 -> T_Either_6 T_TypeError_12 T_Σ_14
MAlonzo.Code.Check.d_inferKind_562
                    (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v1)))
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v2 ->
                    case Any -> T_Σ_14
forall a b. a -> b
coe Any
v2 of
                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v3 Any
v4
                        -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                             ((T_RawTy_2 -> T_Type_16) -> T_RawTy_2 -> Any
forall a b. a -> b
coe
                                T_RawTy_2 -> T_Type_16
d_unconvTy_44
                                (Integer -> T_Weirdℕ_42 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Scoped.d_unshifterTy_360
                                   (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)) (T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
                                   ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
                                      Integer -> T_ScopedTy_14 -> T_RawTy_2
MAlonzo.Code.Scoped.d_extricateScopeTy_780
                                      ((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                         T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Scoped.Extrication.d_len'8902'_4
                                         (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
                                      ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                         T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
MAlonzo.Code.Scoped.Extrication.d_extricateNf'8902'_26
                                         (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v3) (Any -> Any
forall a b. a -> b
coe Any
v4)))))
                      T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))))
-- Evaluator.Term.inferType∅
inferTypeAgda ::
  T_Term_14 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Type_16
inferTypeAgda :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Type_16
inferTypeAgda = (T_Term_14 -> T_Either_6 T_ERROR_12 T_Type_16)
-> T_Term_14 -> T_Either_6 T_ERROR_12 T_Type_16
forall a b. a -> b
coe T_Term_14 -> T_Either_6 T_ERROR_12 T_Type_16
d_inferType'8709'_92
d_inferType'8709'_92 ::
  T_Term_14 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Type_16
d_inferType'8709'_92 :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Type_16
d_inferType'8709'_92 T_Term_14
v0
  = (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 T_Type_16
forall a b. a -> b
coe
      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
      (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
         ((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
         ((Integer
 -> T_Weirdℕ_42
 -> T_RawTm_30
 -> T_Either_6 ScopeError T_ScopedTm_522)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
            Integer
-> T_Weirdℕ_42
-> T_RawTm_30
-> T_Either_6 ScopeError T_ScopedTm_522
MAlonzo.Code.Scoped.d_scopeCheckTm_686 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
            (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
            ((Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Scoped.d_shifter_272 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
               (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44) ((T_Term_14 -> T_RawTm_30) -> T_Term_14 -> Any
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 T_Term_14
v0))))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 ->
            (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
              T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
              (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                 (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                 ((Any -> Any) -> Any
forall a b. a -> b
coe
                    (\ Any
v2 ->
                       (Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                         Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_typeError_14
                         ((T_TypeError_12 -> Text) -> Any -> Any
forall a b. a -> b
coe T_TypeError_12 -> Text
MAlonzo.Code.Evaluator.Base.d_uglyTypeError_24 (Any -> Any
forall a b. a -> b
coe Any
v2))))
                 ((T_Ctx'8902'_2
 -> T_Ctx_2 -> T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                    T_Ctx'8902'_2
-> T_Ctx_2 -> T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14
MAlonzo.Code.Check.d_inferType_1156
                    (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                    (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v1)))
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v2 ->
                    case Any -> T_Σ_14
forall a b. a -> b
coe Any
v2 of
                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v3 Any
v4
                        -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                             ((T_RawTy_2 -> T_Type_16) -> T_RawTy_2 -> Any
forall a b. a -> b
coe
                                T_RawTy_2 -> T_Type_16
d_unconvTy_44
                                (Integer -> T_Weirdℕ_42 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Scoped.d_unshifterTy_360
                                   (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)) (T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
                                   ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
                                      Integer -> T_ScopedTy_14 -> T_RawTy_2
MAlonzo.Code.Scoped.d_extricateScopeTy_780
                                      ((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                         T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Scoped.Extrication.d_len'8902'_4
                                         (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
                                      ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                         T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
MAlonzo.Code.Scoped.Extrication.d_extricateNf'8902'_26
                                         (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                         (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478) (Any -> Any
forall a b. a -> b
coe Any
v3)))))
                      T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))))
-- Evaluator.Term.checkType∅
checkTypeAgda ::
  T_Type_16 ->
  T_Term_14 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
checkTypeAgda :: T_Type_16 -> T_Term_14 -> T_Either_6 T_ERROR_12 ()
checkTypeAgda = (T_Type_16 -> T_Term_14 -> T_Either_6 T_ERROR_12 ())
-> T_Type_16 -> T_Term_14 -> T_Either_6 T_ERROR_12 ()
forall a b. a -> b
coe T_Type_16 -> T_Term_14 -> T_Either_6 T_ERROR_12 ()
d_checkType'8709'_104
d_checkType'8709'_104 ::
  T_Type_16 ->
  T_Term_14 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_checkType'8709'_104 :: T_Type_16 -> T_Term_14 -> T_Either_6 T_ERROR_12 ()
d_checkType'8709'_104 T_Type_16
v0 T_Term_14
v1
  = (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 ()
forall a b. a -> b
coe
      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
      (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
         ((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
         ((Integer -> T_RawTy_2 -> T_Either_6 ScopeError T_ScopedTy_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
            Integer -> T_RawTy_2 -> T_Either_6 ScopeError T_ScopedTy_14
MAlonzo.Code.Scoped.d_scopeCheckTy_616
            ((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
               T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Check.d_len'8902'_106
               (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
            ((Integer -> T_Weirdℕ_42 -> T_RawTy_2 -> T_RawTy_2)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> T_Weirdℕ_42 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Scoped.d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
               (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44) ((T_Type_16 -> T_RawTy_2) -> T_Type_16 -> Any
forall a b. a -> b
coe T_Type_16 -> T_RawTy_2
d_convTy_42 T_Type_16
v0))))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v2 ->
            (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
              T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
              (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                 (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                 ((Any -> Any) -> Any
forall a b. a -> b
coe
                    (\ Any
v3 ->
                       (Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                         Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_typeError_14
                         ((T_TypeError_12 -> Text) -> Any -> Any
forall a b. a -> b
coe T_TypeError_12 -> Text
MAlonzo.Code.Evaluator.Base.d_uglyTypeError_24 (Any -> Any
forall a b. a -> b
coe Any
v3))))
                 ((T_Ctx'8902'_2
 -> T_ScopedTy_14
 -> T_Kind_476
 -> T_Either_6 T_TypeError_12 T__'8866'Nf'8902'__4)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                    T_Ctx'8902'_2
-> T_ScopedTy_14
-> T_Kind_476
-> T_Either_6 T_TypeError_12 T__'8866'Nf'8902'__4
MAlonzo.Code.Check.d_checkKind_554
                    (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v2)
                    (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v3 ->
                    (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                      (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                         (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                         ((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
                         ((Integer
 -> T_Weirdℕ_42
 -> T_RawTm_30
 -> T_Either_6 ScopeError T_ScopedTm_522)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                            Integer
-> T_Weirdℕ_42
-> T_RawTm_30
-> T_Either_6 ScopeError T_ScopedTm_522
MAlonzo.Code.Scoped.d_scopeCheckTm_686 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
                            (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
                            ((Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                               Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Scoped.d_shifter_272 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
                               (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44) ((T_Term_14 -> T_RawTm_30) -> T_Term_14 -> Any
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 T_Term_14
v1))))
                      ((Any -> Any) -> Any
forall a b. a -> b
coe
                         (\ Any
v4 ->
                            (T_Monad_186 -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                              T_Monad_186 -> Any -> Any -> Any
MAlonzo.Code.Utils.du__'62''62'__214
                              (T_Monad_186 -> Any
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.du_EitherP_274)
                              (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                 (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                                 ((Any -> Any) -> Any
forall a b. a -> b
coe
                                    (\ Any
v5 ->
                                       (Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                                         Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_typeError_14
                                         ((T_TypeError_12 -> Text) -> Any -> Any
forall a b. a -> b
coe
                                            T_TypeError_12 -> Text
MAlonzo.Code.Evaluator.Base.d_uglyTypeError_24
                                            (Any -> Any
forall a b. a -> b
coe Any
v5))))
                                 ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T_ScopedTm_522
 -> T__'8866'Nf'8902'__4
 -> T_Either_6 T_TypeError_12 T__'8866'__168)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                    T_Ctx'8902'_2
-> T_Ctx_2
-> T_ScopedTm_522
-> T__'8866'Nf'8902'__4
-> T_Either_6 T_TypeError_12 T__'8866'__168
MAlonzo.Code.Check.d_checkType_1148
                                    (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                    (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v4) (Any -> Any
forall a b. a -> b
coe Any
v3)))
                              ((Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                                 Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                                 (() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))))))))
-- Evaluator.Term.normalizeTypeTerm
normalizeTypeTermAgda ::
  T_Term_14 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Term_14
normalizeTypeTermAgda :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
normalizeTypeTermAgda = (T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14)
-> T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
forall a b. a -> b
coe T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
d_normalizeTypeTerm_120
d_normalizeTypeTerm_120 ::
  T_Term_14 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Term_14
d_normalizeTypeTerm_120 :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
d_normalizeTypeTerm_120 T_Term_14
v0
  = (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 T_Term_14
forall a b. a -> b
coe
      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
      (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
         ((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
         ((Integer
 -> T_Weirdℕ_42
 -> T_RawTm_30
 -> T_Either_6 ScopeError T_ScopedTm_522)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
            Integer
-> T_Weirdℕ_42
-> T_RawTm_30
-> T_Either_6 ScopeError T_ScopedTm_522
MAlonzo.Code.Scoped.d_scopeCheckTm_686 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
            (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
            ((Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Scoped.d_shifter_272 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
               (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44) ((T_Term_14 -> T_RawTm_30) -> T_Term_14 -> Any
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 T_Term_14
v0))))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 ->
            (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
              T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
              (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                 (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                 ((Any -> Any) -> Any
forall a b. a -> b
coe
                    (\ Any
v2 ->
                       (Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                         Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_typeError_14
                         ((T_TypeError_12 -> Text) -> Any -> Any
forall a b. a -> b
coe T_TypeError_12 -> Text
MAlonzo.Code.Evaluator.Base.d_uglyTypeError_24 (Any -> Any
forall a b. a -> b
coe Any
v2))))
                 ((T_Ctx'8902'_2
 -> T_Ctx_2 -> T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                    T_Ctx'8902'_2
-> T_Ctx_2 -> T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14
MAlonzo.Code.Check.d_inferType_1156
                    (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                    (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v1)))
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v2 ->
                    case Any -> T_Σ_14
forall a b. a -> b
coe Any
v2 of
                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v3 Any
v4
                        -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                             ((T_RawTm_30 -> T_Term_14) -> T_RawTm_30 -> Any
forall a b. a -> b
coe
                                T_RawTm_30 -> T_Term_14
d_unconvTm_40
                                (Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Scoped.d_unshifter_434
                                   (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)) (T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
                                   ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
                                      Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
MAlonzo.Code.Scoped.d_extricateScope_828
                                      ((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                         T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Scoped.Extrication.d_len'8902'_4
                                         (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
                                      ((T_Ctx'8902'_2 -> T_Ctx_2 -> T_Weirdℕ_42) -> Any -> Any -> Any
forall a b. a -> b
coe
                                         T_Ctx'8902'_2 -> T_Ctx_2 -> T_Weirdℕ_42
MAlonzo.Code.Scoped.Extrication.d_len_94
                                         (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                         (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4))
                                      ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                         T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
MAlonzo.Code.Scoped.Extrication.d_extricate_140
                                         (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                         (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v3)
                                         (Any -> Any
forall a b. a -> b
coe Any
v4)))))
                      T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))))
-- Evaluator.Term.runTL
runTLAgda ::
  T_Term_14 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Term_14
runTLAgda :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
runTLAgda = (T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14)
-> T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
forall a b. a -> b
coe T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
d_runTL_132
d_runTL_132 ::
  T_Term_14 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Term_14
d_runTL_132 :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
d_runTL_132 T_Term_14
v0
  = (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 T_Term_14
forall a b. a -> b
coe
      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
      (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
         ((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
         ((Integer
 -> T_Weirdℕ_42
 -> T_RawTm_30
 -> T_Either_6 ScopeError T_ScopedTm_522)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
            Integer
-> T_Weirdℕ_42
-> T_RawTm_30
-> T_Either_6 ScopeError T_ScopedTm_522
MAlonzo.Code.Scoped.d_scopeCheckTm_686 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
            (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
            ((Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Scoped.d_shifter_272 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
               (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44) ((T_Term_14 -> T_RawTm_30) -> T_Term_14 -> Any
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 T_Term_14
v0))))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 ->
            (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
              T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
              (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                 (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                 ((Any -> Any) -> Any
forall a b. a -> b
coe
                    (\ Any
v2 ->
                       (Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                         Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_typeError_14
                         ((T_TypeError_12 -> Text) -> Any -> Any
forall a b. a -> b
coe T_TypeError_12 -> Text
MAlonzo.Code.Evaluator.Base.d_uglyTypeError_24 (Any -> Any
forall a b. a -> b
coe Any
v2))))
                 ((T_Ctx'8902'_2
 -> T_Ctx_2 -> T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                    T_Ctx'8902'_2
-> T_Ctx_2 -> T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14
MAlonzo.Code.Check.d_inferType_1156
                    (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                    (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v1)))
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v2 ->
                    case Any -> T_Σ_14
forall a b. a -> b
coe Any
v2 of
                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v3 Any
v4
                        -> (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                             T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                             (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                                ((RuntimeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20)
                                ((T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> Integer
 -> T_Either_6 RuntimeError T__'8866'__168)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                   T__'8866'Nf'8902'__4
-> T__'8866'__168
-> Integer
-> T_Either_6 RuntimeError T__'8866'__168
MAlonzo.Code.Algorithmic.Evaluation.d_stepper_86 (Any -> Any
forall a b. a -> b
coe Any
v3)
                                   (Any -> Any
forall a b. a -> b
coe Any
v4) (Integer -> Any
forall a b. a -> b
coe Integer
MAlonzo.Code.Evaluator.Base.d_maxsteps_72)))
                             ((Any -> Any) -> Any
forall a b. a -> b
coe
                                (\ Any
v5 ->
                                   (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                                     Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                                     ((T_RawTm_30 -> T_Term_14) -> T_RawTm_30 -> Any
forall a b. a -> b
coe
                                        T_RawTm_30 -> T_Term_14
d_unconvTm_40
                                        (Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Scoped.d_unshifter_434
                                           (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)) (T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
                                           ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
                                              Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
MAlonzo.Code.Scoped.d_extricateScope_828
                                              ((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                 T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Scoped.Extrication.d_len'8902'_4
                                                 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
                                              ((T_Ctx'8902'_2 -> T_Ctx_2 -> T_Weirdℕ_42) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                 T_Ctx'8902'_2 -> T_Ctx_2 -> T_Weirdℕ_42
MAlonzo.Code.Scoped.Extrication.d_len_94
                                                 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                                 (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4))
                                              ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                 T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
MAlonzo.Code.Scoped.Extrication.d_extricate_140
                                                 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                                 (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v3)
                                                 (Any -> Any
forall a b. a -> b
coe Any
v5)))))))
                      T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))))
-- Evaluator.Term.runTCK
runTCKAgda ::
  T_Term_14 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Term_14
runTCKAgda :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
runTCKAgda = (T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14)
-> T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
forall a b. a -> b
coe T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
d_runTCK_146
d_runTCK_146 ::
  T_Term_14 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Term_14
d_runTCK_146 :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
d_runTCK_146 T_Term_14
v0
  = (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 T_Term_14
forall a b. a -> b
coe
      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
      (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
         ((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
         ((Integer
 -> T_Weirdℕ_42
 -> T_RawTm_30
 -> T_Either_6 ScopeError T_ScopedTm_522)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
            Integer
-> T_Weirdℕ_42
-> T_RawTm_30
-> T_Either_6 ScopeError T_ScopedTm_522
MAlonzo.Code.Scoped.d_scopeCheckTm_686 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
            (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
            ((Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Scoped.d_shifter_272 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
               (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44) ((T_Term_14 -> T_RawTm_30) -> T_Term_14 -> Any
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 T_Term_14
v0))))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 ->
            (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
              T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
              (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                 (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                 ((Any -> Any) -> Any
forall a b. a -> b
coe
                    (\ Any
v2 ->
                       (Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                         Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_typeError_14
                         ((T_TypeError_12 -> Text) -> Any -> Any
forall a b. a -> b
coe T_TypeError_12 -> Text
MAlonzo.Code.Evaluator.Base.d_uglyTypeError_24 (Any -> Any
forall a b. a -> b
coe Any
v2))))
                 ((T_Ctx'8902'_2
 -> T_Ctx_2 -> T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                    T_Ctx'8902'_2
-> T_Ctx_2 -> T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14
MAlonzo.Code.Check.d_inferType_1156
                    (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                    (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v1)))
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v2 ->
                    case Any -> T_Σ_14
forall a b. a -> b
coe Any
v2 of
                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v3 Any
v4
                        -> (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                             T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                             (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                                ((RuntimeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20)
                                ((Integer -> T_State_34 -> T_Either_6 RuntimeError T_State_34)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                   Integer -> T_State_34 -> T_Either_6 RuntimeError T_State_34
MAlonzo.Code.Algorithmic.CK.du_stepper_372
                                   (Integer -> Any
forall a b. a -> b
coe Integer
MAlonzo.Code.Evaluator.Base.d_maxsteps_72)
                                   ((T__'8866'Nf'8902'__4
 -> T_Stack_18 -> T__'8866'__168 -> T_State_34)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                      T__'8866'Nf'8902'__4 -> T_Stack_18 -> T__'8866'__168 -> T_State_34
MAlonzo.Code.Algorithmic.CK.C__'9659'__40 (Any -> Any
forall a b. a -> b
coe Any
v3)
                                      (T_Stack_18 -> Any
forall a b. a -> b
coe T_Stack_18
MAlonzo.Code.Algorithmic.CK.C_ε_22) (Any -> Any
forall a b. a -> b
coe Any
v4))))
                             ((Any -> Any) -> Any
forall a b. a -> b
coe
                                (\ Any
v5 ->
                                   case Any -> T_State_34
forall a b. a -> b
coe Any
v5 of
                                     MAlonzo.Code.Algorithmic.CK.C__'9659'__40 T__'8866'Nf'8902'__4
v6 T_Stack_18
v7 T__'8866'__168
v8
                                       -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                                            Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                                            ((RuntimeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                                               RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20
                                               (RuntimeError -> Any
forall a b. a -> b
coe RuntimeError
MAlonzo.Code.Utils.C_gasError_350))
                                     MAlonzo.Code.Algorithmic.CK.C__'9669'__46 T__'8866'Nf'8902'__4
v6 T_Stack_18
v7 T__'8866'__168
v8 T_Value_28
v9
                                       -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                                            Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                                            ((RuntimeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                                               RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20
                                               (RuntimeError -> Any
forall a b. a -> b
coe RuntimeError
MAlonzo.Code.Utils.C_gasError_350))
                                     MAlonzo.Code.Algorithmic.CK.C_'9633'_50 T__'8866'__168
v6 T_Value_28
v7
                                       -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                                            Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                                            ((T_RawTm_30 -> T_Term_14) -> T_RawTm_30 -> Any
forall a b. a -> b
coe
                                               T_RawTm_30 -> T_Term_14
d_unconvTm_40
                                               (Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Scoped.d_unshifter_434
                                                  (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer))
                                                  (T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
                                                  ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
                                                     Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
MAlonzo.Code.Scoped.d_extricateScope_828
                                                     ((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                        T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Scoped.Extrication.d_len'8902'_4
                                                        (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
                                                     ((T_Ctx'8902'_2 -> T_Ctx_2 -> T_Weirdℕ_42) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                        T_Ctx'8902'_2 -> T_Ctx_2 -> T_Weirdℕ_42
MAlonzo.Code.Scoped.Extrication.d_len_94
                                                        (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                                        (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4))
                                                     ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                        T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
MAlonzo.Code.Scoped.Extrication.d_extricate_140
                                                        (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                                        (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4)
                                                        (Any -> Any
forall a b. a -> b
coe Any
v3) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v6)))))
                                     MAlonzo.Code.Algorithmic.CK.C_'9670'_54 T__'8866'Nf'8902'__4
v6
                                       -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                                            Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                                            ((T_RawTm_30 -> T_Term_14) -> T_RawTm_30 -> Any
forall a b. a -> b
coe
                                               T_RawTm_30 -> T_Term_14
d_unconvTm_40
                                               (Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Scoped.d_unshifter_434
                                                  (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer))
                                                  (T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
                                                  ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
                                                     Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
MAlonzo.Code.Scoped.d_extricateScope_828
                                                     (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
                                                     (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
                                                     ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                        T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
MAlonzo.Code.Scoped.Extrication.d_extricate_140
                                                        (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                                        (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4)
                                                        (Any -> Any
forall a b. a -> b
coe Any
v3)
                                                        (T__'8866'__168 -> Any
forall a b. a -> b
coe
                                                           T__'8866'__168
MAlonzo.Code.Algorithmic.C_error_258)))))
                                     T_State_34
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
                      T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))))
-- Evaluator.Term.runTCEK
runTCEKAgda ::
  T_Term_14 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Term_14
runTCEKAgda :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
runTCEKAgda = (T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14)
-> T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
forall a b. a -> b
coe T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
d_runTCEK_166
d_runTCEK_166 ::
  T_Term_14 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Term_14
d_runTCEK_166 :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
d_runTCEK_166 T_Term_14
v0
  = (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 T_Term_14
forall a b. a -> b
coe
      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
      (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
         ((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
         ((Integer
 -> T_Weirdℕ_42
 -> T_RawTm_30
 -> T_Either_6 ScopeError T_ScopedTm_522)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
            Integer
-> T_Weirdℕ_42
-> T_RawTm_30
-> T_Either_6 ScopeError T_ScopedTm_522
MAlonzo.Code.Scoped.d_scopeCheckTm_686 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
            (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
            ((Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
               Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Scoped.d_shifter_272 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
               (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44) ((T_Term_14 -> T_RawTm_30) -> T_Term_14 -> Any
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 T_Term_14
v0))))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 ->
            (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
              T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
              (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                 (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                 ((Any -> Any) -> Any
forall a b. a -> b
coe
                    (\ Any
v2 ->
                       (Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                         Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_typeError_14
                         ((T_TypeError_12 -> Text) -> Any -> Any
forall a b. a -> b
coe T_TypeError_12 -> Text
MAlonzo.Code.Evaluator.Base.d_uglyTypeError_24 (Any -> Any
forall a b. a -> b
coe Any
v2))))
                 ((T_Ctx'8902'_2
 -> T_Ctx_2 -> T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                    T_Ctx'8902'_2
-> T_Ctx_2 -> T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14
MAlonzo.Code.Check.d_inferType_1156
                    (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                    (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v1)))
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v2 ->
                    case Any -> T_Σ_14
forall a b. a -> b
coe Any
v2 of
                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v3 Any
v4
                        -> (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                             T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                             (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                                ((RuntimeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20)
                                ((Integer -> T_State_1180 -> T_Either_6 RuntimeError T_State_1180)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                   Integer -> T_State_1180 -> T_Either_6 RuntimeError T_State_1180
MAlonzo.Code.Algorithmic.CEK.du_stepper_1532
                                   (Integer -> Any
forall a b. a -> b
coe Integer
MAlonzo.Code.Evaluator.Base.d_maxsteps_72)
                                   ((T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T_Stack_1166
 -> T_Env_26
 -> T__'8866'__168
 -> T_State_1180)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                      T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Stack_1166
-> T_Env_26
-> T__'8866'__168
-> T_State_1180
MAlonzo.Code.Algorithmic.CEK.C__'894'_'9659'__1188
                                      (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v3)
                                      (T_Stack_1166 -> Any
forall a b. a -> b
coe T_Stack_1166
MAlonzo.Code.Algorithmic.CEK.C_ε_1170)
                                      (T_Env_26 -> Any
forall a b. a -> b
coe T_Env_26
MAlonzo.Code.Algorithmic.CEK.C_'91''93'_202) (Any -> Any
forall a b. a -> b
coe Any
v4))))
                             ((Any -> Any) -> Any
forall a b. a -> b
coe
                                (\ Any
v5 ->
                                   case Any -> T_State_1180
forall a b. a -> b
coe Any
v5 of
                                     MAlonzo.Code.Algorithmic.CEK.C__'894'_'9659'__1188 T_Ctx_2
v6 T__'8866'Nf'8902'__4
v7 T_Stack_1166
v8 T_Env_26
v9 T__'8866'__168
v10
                                       -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                                            Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                                            ((RuntimeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                                               RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20
                                               (RuntimeError -> Any
forall a b. a -> b
coe RuntimeError
MAlonzo.Code.Utils.C_gasError_350))
                                     MAlonzo.Code.Algorithmic.CEK.C__'9669'__1192 T__'8866'Nf'8902'__4
v6 T_Stack_1166
v7 T_Value_52
v8
                                       -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                                            Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                                            ((RuntimeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                                               RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20
                                               (RuntimeError -> Any
forall a b. a -> b
coe RuntimeError
MAlonzo.Code.Utils.C_gasError_350))
                                     MAlonzo.Code.Algorithmic.CEK.C_'9633'_1194 T_Value_52
v6
                                       -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                                            Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                                            ((T_RawTm_30 -> T_Term_14) -> T_RawTm_30 -> Any
forall a b. a -> b
coe
                                               T_RawTm_30 -> T_Term_14
d_unconvTm_40
                                               (Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Scoped.d_unshifter_434
                                                  (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer))
                                                  (T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
                                                  ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
                                                     Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
MAlonzo.Code.Scoped.d_extricateScope_828
                                                     ((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                        T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Scoped.Extrication.d_len'8902'_4
                                                        (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
                                                     ((T_Ctx'8902'_2 -> T_Ctx_2 -> T_Weirdℕ_42) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                        T_Ctx'8902'_2 -> T_Ctx_2 -> T_Weirdℕ_42
MAlonzo.Code.Scoped.Extrication.d_len_94
                                                        (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                                        (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4))
                                                     ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                        T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
MAlonzo.Code.Scoped.Extrication.d_extricate_140
                                                        (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                                        (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4)
                                                        (Any -> Any
forall a b. a -> b
coe Any
v3)
                                                        ((T__'8866'Nf'8902'__4 -> T_Value_52 -> T__'8866'__168)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                           T__'8866'Nf'8902'__4 -> T_Value_52 -> T__'8866'__168
MAlonzo.Code.Algorithmic.CEK.d_discharge_228
                                                           (Any -> Any
forall a b. a -> b
coe Any
v3) (T_Value_52 -> Any
forall a b. a -> b
coe T_Value_52
v6))))))
                                     MAlonzo.Code.Algorithmic.CEK.C_'9670'_1196 T__'8866'Nf'8902'__4
v6
                                       -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                                            Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                                            ((T_RawTm_30 -> T_Term_14) -> T_RawTm_30 -> Any
forall a b. a -> b
coe
                                               T_RawTm_30 -> T_Term_14
d_unconvTm_40
                                               (Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Scoped.d_unshifter_434
                                                  (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer))
                                                  (T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
                                                  ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
                                                     Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
MAlonzo.Code.Scoped.d_extricateScope_828
                                                     (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
                                                     (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
                                                     ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                        T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
MAlonzo.Code.Scoped.Extrication.d_extricate_140
                                                        (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                                        (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4)
                                                        (Any -> Any
forall a b. a -> b
coe Any
v3)
                                                        (T__'8866'__168 -> Any
forall a b. a -> b
coe
                                                           T__'8866'__168
MAlonzo.Code.Algorithmic.C_error_258)))))
                                     T_State_1180
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
                      T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))))
-- Evaluator.Term.runUValue
d_runUValue_186 ::
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Untyped.CEK.T_Value_14
d_runUValue_186 :: T__'8866'_14 -> T_Either_6 T_ERROR_12 T_Value_14
d_runUValue_186 T__'8866'_14
v0
  = (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 T_Value_14
forall a b. a -> b
coe
      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
      (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
         ((RuntimeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20)
         ((Integer -> T_State_218 -> T_Either_6 RuntimeError T_State_218)
-> Any -> Any -> Any
forall a b. a -> b
coe
            Integer -> T_State_218 -> T_Either_6 RuntimeError T_State_218
MAlonzo.Code.Untyped.CEK.d_stepper_1234
            (Integer -> Any
forall a b. a -> b
coe Integer
MAlonzo.Code.Evaluator.Base.d_maxsteps_72)
            ((T_Stack_6 -> T_Env_16 -> T__'8866'_14 -> T_State_218)
-> Any -> Any -> T__'8866'_14 -> Any
forall a b. a -> b
coe
               T_Stack_6 -> T_Env_16 -> T__'8866'_14 -> T_State_218
MAlonzo.Code.Untyped.CEK.C__'894'_'9659'__222
               (T_Stack_6 -> Any
forall a b. a -> b
coe T_Stack_6
MAlonzo.Code.Untyped.CEK.C_ε_10)
               (T_Env_16 -> Any
forall a b. a -> b
coe T_Env_16
MAlonzo.Code.Untyped.CEK.C_'91''93'_18) T__'8866'_14
v0)))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 ->
            let v2 :: t
v2
                  = (Any -> T_Either_6 Any Any) -> Any -> t
forall a b. a -> b
coe
                      Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                      ((RuntimeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                         RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20
                         (RuntimeError -> Any
forall a b. a -> b
coe RuntimeError
MAlonzo.Code.Utils.C_gasError_350)) in
            Any -> Any
forall a b. a -> b
coe
              (case Any -> T_State_218
forall a b. a -> b
coe Any
v1 of
                 MAlonzo.Code.Untyped.CEK.C_'9633'_226 T_Value_14
v3
                   -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 (T_Value_14 -> Any
forall a b. a -> b
coe T_Value_14
v3)
                 T_State_218
MAlonzo.Code.Untyped.CEK.C_'9670'_228
                   -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                        Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                        ((RuntimeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                           RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20
                           (RuntimeError -> Any
forall a b. a -> b
coe RuntimeError
MAlonzo.Code.Utils.C_userError_352))
                 T_State_218
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2)))
-- Evaluator.Term.runU
runUAgda ::
  T_TermU_24 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_TermU_24
runUAgda :: T_TermU_24 -> T_Either_6 T_ERROR_12 T_TermU_24
runUAgda = (T_TermU_24 -> T_Either_6 T_ERROR_12 T_TermU_24)
-> T_TermU_24 -> T_Either_6 T_ERROR_12 T_TermU_24
forall a b. a -> b
coe T_TermU_24 -> T_Either_6 T_ERROR_12 T_TermU_24
d_runU_194
d_runU_194 ::
  T_TermU_24 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_TermU_24
d_runU_194 :: T_TermU_24 -> T_Either_6 T_ERROR_12 T_TermU_24
d_runU_194 T_TermU_24
v0
  = (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 T_TermU_24
forall a b. a -> b
coe
      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
      (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
         ((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
         ((T_Untyped_146 -> T_Either_6 ScopeError T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
            T_Untyped_146 -> T_Either_6 ScopeError T__'8866'_14
MAlonzo.Code.Untyped.d_scopeCheckU0_304 ((T_TermU_24 -> T_Untyped_146) -> T_TermU_24 -> Any
forall a b. a -> b
coe T_TermU_24 -> T_Untyped_146
d_convTmU_46 T_TermU_24
v0)))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 ->
            (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
              T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42 ((T__'8866'_14 -> T_Either_6 T_ERROR_12 T_Value_14) -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T_Either_6 T_ERROR_12 T_Value_14
d_runUValue_186 (Any -> Any
forall a b. a -> b
coe Any
v1))
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v2 ->
                    (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                      Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                      ((T_Untyped_146 -> T_TermU_24) -> T_Untyped_146 -> Any
forall a b. a -> b
coe
                         T_Untyped_146 -> T_TermU_24
d_unconvTmU_48
                         (T__'8866'_14 -> T_Untyped_146
MAlonzo.Code.Untyped.d_extricateU0_218
                            ((T_Value_14 -> T__'8866'_14) -> Any -> T__'8866'_14
forall a b. a -> b
coe T_Value_14 -> T__'8866'_14
MAlonzo.Code.Untyped.CEK.d_discharge_126 (Any -> Any
forall a b. a -> b
coe Any
v2))))))))
-- Evaluator.Term.runUCounting
runUCountingAgda ::
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
    (MAlonzo.Code.Utils.T_List_382
       (MAlonzo.Code.Utils.T__'215'__364
          MAlonzo.Code.Agda.Builtin.String.T_String_6
          MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_146)) ->
  T_TermU_24 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    (MAlonzo.Code.Utils.T__'215'__364
       T_TermU_24 (MAlonzo.Code.Utils.T__'215'__364 Integer Integer))
runUCountingAgda :: T__'215'__364
  T_HCekMachineCosts_4
  (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
-> T_TermU_24
-> T_Either_6
     T_ERROR_12
     (T__'215'__364 T_TermU_24 (T__'215'__364 Integer Integer))
runUCountingAgda = (T__'215'__364
   T_HCekMachineCosts_4
   (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
 -> T_TermU_24
 -> T_Either_6
      T_ERROR_12
      (T__'215'__364 T_TermU_24 (T__'215'__364 Integer Integer)))
-> T__'215'__364
     T_HCekMachineCosts_4
     (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
-> T_TermU_24
-> T_Either_6
     T_ERROR_12
     (T__'215'__364 T_TermU_24 (T__'215'__364 Integer Integer))
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4
  (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
-> T_TermU_24
-> T_Either_6
     T_ERROR_12
     (T__'215'__364 T_TermU_24 (T__'215'__364 Integer Integer))
d_runUCounting_202
d_runUCounting_202 ::
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
    (MAlonzo.Code.Utils.T_List_382
       (MAlonzo.Code.Utils.T__'215'__364
          MAlonzo.Code.Agda.Builtin.String.T_String_6
          MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_146)) ->
  T_TermU_24 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    (MAlonzo.Code.Utils.T__'215'__364
       T_TermU_24 (MAlonzo.Code.Utils.T__'215'__364 Integer Integer))
d_runUCounting_202 :: T__'215'__364
  T_HCekMachineCosts_4
  (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
-> T_TermU_24
-> T_Either_6
     T_ERROR_12
     (T__'215'__364 T_TermU_24 (T__'215'__364 Integer Integer))
d_runUCounting_202 T__'215'__364
  T_HCekMachineCosts_4
  (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
v0 T_TermU_24
v1
  = case T__'215'__364
  T_HCekMachineCosts_4
  (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
-> (Any, Any)
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4
  (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
v0 of
      MAlonzo.Code.Utils.C__'44'__378 Any
v2 Any
v3
        -> let v4 :: t
v4
                 = ((Any -> Any) -> Any -> Maybe Any -> Any) -> Any -> Any -> Any -> t
forall a b. a -> b
coe
                     (Any -> Any) -> Any -> Maybe Any -> Any
MAlonzo.Code.Data.Maybe.Base.du_maybe_32
                     ((Any -> Any) -> Any
forall a b. a -> b
coe
                        (\ Any
v4 ->
                           (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                             (([T_Σ_14] -> DefaultFun -> T_BuiltinModel_60) -> Any -> Any
forall a b. a -> b
coe [T_Σ_14] -> DefaultFun -> T_BuiltinModel_60
MAlonzo.Code.Cost.Model.d_lookupModel_446 (Any -> Any
forall a b. a -> b
coe Any
v4))))
                     (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
                     (([Maybe Any] -> Maybe [Any]) -> Any -> Any
forall a b. a -> b
coe
                        [Maybe Any] -> Maybe [Any]
MAlonzo.Code.Cost.Model.du_allJust_482
                        ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                           Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                           ((DefaultFun
 -> T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)
 -> Maybe T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
                              DefaultFun
-> T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)
-> Maybe T_Σ_14
MAlonzo.Code.Cost.Model.d_getModel_404
                              (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
MAlonzo.Code.Builtin.C_addInteger_4) (Any -> Any
forall a b. a -> b
coe Any
v3))
                           (((Any -> Any) -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                              (Any -> Any) -> [Any] -> [Any]
MAlonzo.Code.Data.List.Base.du_map_22
                              ((Any -> Maybe T_Σ_14) -> Any
forall a b. a -> b
coe
                                 (\ Any
v4 -> DefaultFun
-> T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)
-> Maybe T_Σ_14
MAlonzo.Code.Cost.Model.d_getModel_404 (Any -> DefaultFun
forall a b. a -> b
coe Any
v4) (Any -> T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)
forall a b. a -> b
coe Any
v3)))
                              ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                 Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                 (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
MAlonzo.Code.Builtin.C_subtractInteger_6)
                                 ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                    Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                    (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
MAlonzo.Code.Builtin.C_multiplyInteger_8)
                                    ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                       Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                       (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
MAlonzo.Code.Builtin.C_divideInteger_10)
                                       ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                          Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                          (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
MAlonzo.Code.Builtin.C_quotientInteger_12)
                                          ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                             (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
MAlonzo.Code.Builtin.C_remainderInteger_14)
                                             ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
MAlonzo.Code.Builtin.C_modInteger_16)
                                                ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                   Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                   (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
MAlonzo.Code.Builtin.C_equalsInteger_18)
                                                   ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                      Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                      (DefaultFun -> Any
forall a b. a -> b
coe
                                                         DefaultFun
MAlonzo.Code.Builtin.C_lessThanInteger_20)
                                                      ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                         Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                         (DefaultFun -> Any
forall a b. a -> b
coe
                                                            DefaultFun
MAlonzo.Code.Builtin.C_lessThanEqualsInteger_22)
                                                         ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                            Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                            (DefaultFun -> Any
forall a b. a -> b
coe
                                                               DefaultFun
MAlonzo.Code.Builtin.C_appendByteString_24)
                                                            ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                               Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                               (DefaultFun -> Any
forall a b. a -> b
coe
                                                                  DefaultFun
MAlonzo.Code.Builtin.C_consByteString_26)
                                                               ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                  Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                  (DefaultFun -> Any
forall a b. a -> b
coe
                                                                     DefaultFun
MAlonzo.Code.Builtin.C_sliceByteString_28)
                                                                  ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                     Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                     (DefaultFun -> Any
forall a b. a -> b
coe
                                                                        DefaultFun
MAlonzo.Code.Builtin.C_lengthOfByteString_30)
                                                                     ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                        Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                        (DefaultFun -> Any
forall a b. a -> b
coe
                                                                           DefaultFun
MAlonzo.Code.Builtin.C_indexByteString_32)
                                                                        ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                           Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                           (DefaultFun -> Any
forall a b. a -> b
coe
                                                                              DefaultFun
MAlonzo.Code.Builtin.C_equalsByteString_34)
                                                                           ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                              Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                              (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                 DefaultFun
MAlonzo.Code.Builtin.C_lessThanByteString_36)
                                                                              ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                 Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                 (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                    DefaultFun
MAlonzo.Code.Builtin.C_lessThanEqualsByteString_38)
                                                                                 ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                    Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                    (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                       DefaultFun
MAlonzo.Code.Builtin.C_sha2'45'256_40)
                                                                                    ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                       Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                       (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                          DefaultFun
MAlonzo.Code.Builtin.C_sha3'45'256_42)
                                                                                       ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                          Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                          (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                             DefaultFun
MAlonzo.Code.Builtin.C_blake2b'45'256_44)
                                                                                          ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                             (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                DefaultFun
MAlonzo.Code.Builtin.C_verifyEd25519Signature_46)
                                                                                             ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                   DefaultFun
MAlonzo.Code.Builtin.C_verifyEcdsaSecp256k1Signature_48)
                                                                                                ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                   Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                   (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                      DefaultFun
MAlonzo.Code.Builtin.C_verifySchnorrSecp256k1Signature_50)
                                                                                                   ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                      Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                      (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                         DefaultFun
MAlonzo.Code.Builtin.C_appendString_52)
                                                                                                      ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                         Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                         (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                            DefaultFun
MAlonzo.Code.Builtin.C_equalsString_54)
                                                                                                         ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                            Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                            (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                               DefaultFun
MAlonzo.Code.Builtin.C_encodeUtf8_56)
                                                                                                            ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                               Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                               (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                  DefaultFun
MAlonzo.Code.Builtin.C_decodeUtf8_58)
                                                                                                               ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                  Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                  (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                     DefaultFun
MAlonzo.Code.Builtin.C_ifThenElse_60)
                                                                                                                  ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                     Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                     (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                        DefaultFun
MAlonzo.Code.Builtin.C_chooseUnit_62)
                                                                                                                     ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                        Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                        (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                           DefaultFun
MAlonzo.Code.Builtin.C_trace_64)
                                                                                                                        ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                           Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                           (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                              DefaultFun
MAlonzo.Code.Builtin.C_fstPair_66)
                                                                                                                           ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                              Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                              (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                 DefaultFun
MAlonzo.Code.Builtin.C_sndPair_68)
                                                                                                                              ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                 Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                 (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                    DefaultFun
MAlonzo.Code.Builtin.C_chooseList_70)
                                                                                                                                 ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                    Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                    (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                       DefaultFun
MAlonzo.Code.Builtin.C_mkCons_72)
                                                                                                                                    ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                       Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                       (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                          DefaultFun
MAlonzo.Code.Builtin.C_headList_74)
                                                                                                                                       ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                          Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                          (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                             DefaultFun
MAlonzo.Code.Builtin.C_tailList_76)
                                                                                                                                          ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                             (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                DefaultFun
MAlonzo.Code.Builtin.C_nullList_78)
                                                                                                                                             ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                   DefaultFun
MAlonzo.Code.Builtin.C_chooseData_80)
                                                                                                                                                ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                   Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                   (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                      DefaultFun
MAlonzo.Code.Builtin.C_constrData_82)
                                                                                                                                                   ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                      Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                      (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                         DefaultFun
MAlonzo.Code.Builtin.C_mapData_84)
                                                                                                                                                      ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                         Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                         (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                            DefaultFun
MAlonzo.Code.Builtin.C_listData_86)
                                                                                                                                                         ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                            Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                            (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                               DefaultFun
MAlonzo.Code.Builtin.C_iData_88)
                                                                                                                                                            ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                               Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                               (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                  DefaultFun
MAlonzo.Code.Builtin.C_bData_90)
                                                                                                                                                               ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                  Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                  (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                     DefaultFun
MAlonzo.Code.Builtin.C_unConstrData_92)
                                                                                                                                                                  ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                     Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                     (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                        DefaultFun
MAlonzo.Code.Builtin.C_unMapData_94)
                                                                                                                                                                     ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                        Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                        (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                           DefaultFun
MAlonzo.Code.Builtin.C_unListData_96)
                                                                                                                                                                        ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                           Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                           (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                              DefaultFun
MAlonzo.Code.Builtin.C_unIData_98)
                                                                                                                                                                           ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                              Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                              (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                 DefaultFun
MAlonzo.Code.Builtin.C_unBData_100)
                                                                                                                                                                              ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                 Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                 (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                    DefaultFun
MAlonzo.Code.Builtin.C_equalsData_102)
                                                                                                                                                                                 ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                    Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                    (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                       DefaultFun
MAlonzo.Code.Builtin.C_serialiseData_104)
                                                                                                                                                                                    ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                       Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                       (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                          DefaultFun
MAlonzo.Code.Builtin.C_mkPairData_106)
                                                                                                                                                                                       ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                          Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                          (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                             DefaultFun
MAlonzo.Code.Builtin.C_mkNilData_108)
                                                                                                                                                                                          ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                             (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                DefaultFun
MAlonzo.Code.Builtin.C_mkNilPairData_110)
                                                                                                                                                                                             ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                   DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G1'45'add_112)
                                                                                                                                                                                                ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                   Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                   (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                      DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G1'45'neg_114)
                                                                                                                                                                                                   ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                      Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                      (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                         DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G1'45'scalarMul_116)
                                                                                                                                                                                                      ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                         Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                         (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                            DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G1'45'equal_118)
                                                                                                                                                                                                         ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                            Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                            (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                               DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G1'45'hashToGroup_120)
                                                                                                                                                                                                            ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                               Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                               (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                  DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G1'45'compress_122)
                                                                                                                                                                                                               ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                  Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                  (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                     DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G1'45'uncompress_124)
                                                                                                                                                                                                                  ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                     Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                     (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                        DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G2'45'add_126)
                                                                                                                                                                                                                     ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                        Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                        (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                           DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G2'45'neg_128)
                                                                                                                                                                                                                        ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                           Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                           (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                              DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G2'45'scalarMul_130)
                                                                                                                                                                                                                           ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                              Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                              (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                 DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G2'45'equal_132)
                                                                                                                                                                                                                              ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                 Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                 (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                    DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G2'45'hashToGroup_134)
                                                                                                                                                                                                                                 ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                    Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                    (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                       DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G2'45'compress_136)
                                                                                                                                                                                                                                    ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                       Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                       (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                          DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G2'45'uncompress_138)
                                                                                                                                                                                                                                       ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                          Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                          (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                             DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'millerLoop_140)
                                                                                                                                                                                                                                          ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                             (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'mulMlResult_142)
                                                                                                                                                                                                                                             ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                   DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'finalVerify_144)
                                                                                                                                                                                                                                                ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                   Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                   (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                      DefaultFun
MAlonzo.Code.Builtin.C_keccak'45'256_146)
                                                                                                                                                                                                                                                   ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                      Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                      (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                         DefaultFun
MAlonzo.Code.Builtin.C_blake2b'45'224_148)
                                                                                                                                                                                                                                                      ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                         Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                         (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                            DefaultFun
MAlonzo.Code.Builtin.C_byteStringToInteger_150)
                                                                                                                                                                                                                                                         ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                            Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                            (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                               DefaultFun
MAlonzo.Code.Builtin.C_integerToByteString_152)
                                                                                                                                                                                                                                                            ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                               Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                               (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                  DefaultFun
MAlonzo.Code.Builtin.C_andByteString_154)
                                                                                                                                                                                                                                                               ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                  Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                  (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                     DefaultFun
MAlonzo.Code.Builtin.C_orByteString_156)
                                                                                                                                                                                                                                                                  ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                     Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                     (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                        DefaultFun
MAlonzo.Code.Builtin.C_xorByteString_158)
                                                                                                                                                                                                                                                                     ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                        Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                        (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                           DefaultFun
MAlonzo.Code.Builtin.C_complementByteString_160)
                                                                                                                                                                                                                                                                        ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                           Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                           (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                              DefaultFun
MAlonzo.Code.Builtin.C_readBit_162)
                                                                                                                                                                                                                                                                           ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                              Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                              (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                 DefaultFun
MAlonzo.Code.Builtin.C_writeBits_164)
                                                                                                                                                                                                                                                                              ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                 Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                                 (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                    DefaultFun
MAlonzo.Code.Builtin.C_replicateByte_166)
                                                                                                                                                                                                                                                                                 ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                    Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                                    (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                       DefaultFun
MAlonzo.Code.Builtin.C_shiftByteString_168)
                                                                                                                                                                                                                                                                                    ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                       Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                                       (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                          DefaultFun
MAlonzo.Code.Builtin.C_rotateByteString_170)
                                                                                                                                                                                                                                                                                       ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                          Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                                          (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                             DefaultFun
MAlonzo.Code.Builtin.C_countSetBits_172)
                                                                                                                                                                                                                                                                                          ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                                             (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                                DefaultFun
MAlonzo.Code.Builtin.C_findFirstSetBit_174)
                                                                                                                                                                                                                                                                                             ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                                Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                                                (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                                   DefaultFun
MAlonzo.Code.Builtin.C_ripemd'45'160_176)
                                                                                                                                                                                                                                                                                                ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                                   Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                                                   (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                                      DefaultFun
MAlonzo.Code.Builtin.C_expModInteger_178)
                                                                                                                                                                                                                                                                                                   ([Any] -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                                      [Any]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in
           Any
-> T_Either_6
     T_ERROR_12
     (T__'215'__364 T_TermU_24 (T__'215'__364 Integer Integer))
forall a b. a -> b
coe
             (case Any -> Maybe Any
forall a b. a -> b
coe Any
forall a. a
v4 of
                MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v5
                  -> (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                       (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                          (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                          ((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
                          ((T_Untyped_146 -> T_Either_6 ScopeError T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                             T_Untyped_146 -> T_Either_6 ScopeError T__'8866'_14
MAlonzo.Code.Untyped.d_scopeCheckU0_304 ((T_TermU_24 -> T_Untyped_146) -> T_TermU_24 -> Any
forall a b. a -> b
coe T_TermU_24 -> T_Untyped_146
d_convTmU_46 T_TermU_24
v1)))
                       ((Any -> Any) -> Any
forall a b. a -> b
coe
                          (\ Any
v6 ->
                             (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                               T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                               (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                  (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                                  ((RuntimeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20)
                                  ((T_Writer_304 -> Any) -> Any -> Any
forall a b. a -> b
coe
                                     T_Writer_304 -> Any
MAlonzo.Code.Utils.d_wrvalue_314
                                     ((T_MachineParameters_46 -> Integer -> T_State_218 -> T_Writer_304)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                        T_MachineParameters_46 -> Integer -> T_State_218 -> T_Writer_304
MAlonzo.Code.Untyped.CEKWithCost.du_stepperC_338
                                        ((T__'215'__364
   T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
 -> T_MachineParameters_46)
-> Any -> Any
forall a b. a -> b
coe
                                           T__'215'__364
  T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
-> T_MachineParameters_46
MAlonzo.Code.Cost.d_machineParameters_140
                                           ((Any -> Any -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378 (Any -> Any
forall a b. a -> b
coe Any
v2) (Any -> Any
forall a b. a -> b
coe Any
v5)))
                                        (Integer -> Any
forall a b. a -> b
coe Integer
MAlonzo.Code.Evaluator.Base.d_maxsteps_72)
                                        ((T_Stack_6 -> T_Env_16 -> T__'8866'_14 -> T_State_218)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                           T_Stack_6 -> T_Env_16 -> T__'8866'_14 -> T_State_218
MAlonzo.Code.Untyped.CEK.C__'894'_'9659'__222
                                           (T_Stack_6 -> Any
forall a b. a -> b
coe T_Stack_6
MAlonzo.Code.Untyped.CEK.C_ε_10)
                                           (T_Env_16 -> Any
forall a b. a -> b
coe T_Env_16
MAlonzo.Code.Untyped.CEK.C_'91''93'_18) Any
v6))))
                               ((Any -> Any) -> Any
forall a b. a -> b
coe
                                  (\ Any
v7 ->
                                     let v8 :: t
v8
                                           = (Any -> T_Either_6 Any Any) -> Any -> t
forall a b. a -> b
coe
                                               Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                                               ((RuntimeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                                                  RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20
                                                  (RuntimeError -> Any
forall a b. a -> b
coe RuntimeError
MAlonzo.Code.Utils.C_gasError_350)) in
                                     Any -> Any
forall a b. a -> b
coe
                                       (case Any -> T_State_218
forall a b. a -> b
coe Any
v7 of
                                          MAlonzo.Code.Untyped.CEK.C_'9633'_226 T_Value_14
v9
                                            -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                                                 Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                                                 ((Any -> Any -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                    Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378
                                                    ((T_Untyped_146 -> T_TermU_24) -> T_Untyped_146 -> Any
forall a b. a -> b
coe
                                                       T_Untyped_146 -> T_TermU_24
d_unconvTmU_48
                                                       (T__'8866'_14 -> T_Untyped_146
MAlonzo.Code.Untyped.d_extricateU0_218
                                                          ((T_Value_14 -> T__'8866'_14) -> Any -> T__'8866'_14
forall a b. a -> b
coe
                                                             T_Value_14 -> T__'8866'_14
MAlonzo.Code.Untyped.CEK.d_discharge_126
                                                             (T_Value_14 -> Any
forall a b. a -> b
coe T_Value_14
v9))))
                                                    ((Any -> Any -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                       Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378
                                                       ((T_ExBudget_52 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                          T_ExBudget_52 -> Integer
MAlonzo.Code.Cost.d_ExCPU_58
                                                          ((T_Writer_304 -> Any) -> Any -> Any
forall a b. a -> b
coe
                                                             T_Writer_304 -> Any
MAlonzo.Code.Utils.d_accum_316
                                                             ((T_MachineParameters_46 -> Integer -> T_State_218 -> T_Writer_304)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                T_MachineParameters_46 -> Integer -> T_State_218 -> T_Writer_304
MAlonzo.Code.Untyped.CEKWithCost.du_stepperC_338
                                                                ((T__'215'__364
   T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
 -> T_MachineParameters_46)
-> Any -> Any
forall a b. a -> b
coe
                                                                   T__'215'__364
  T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
-> T_MachineParameters_46
MAlonzo.Code.Cost.d_machineParameters_140
                                                                   ((Any -> Any -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                      Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378
                                                                      (Any -> Any
forall a b. a -> b
coe Any
v2) (Any -> Any
forall a b. a -> b
coe Any
v5)))
                                                                (Integer -> Any
forall a b. a -> b
coe
                                                                   Integer
MAlonzo.Code.Evaluator.Base.d_maxsteps_72)
                                                                ((T_Stack_6 -> T_Env_16 -> T__'8866'_14 -> T_State_218)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                   T_Stack_6 -> T_Env_16 -> T__'8866'_14 -> T_State_218
MAlonzo.Code.Untyped.CEK.C__'894'_'9659'__222
                                                                   (T_Stack_6 -> Any
forall a b. a -> b
coe
                                                                      T_Stack_6
MAlonzo.Code.Untyped.CEK.C_ε_10)
                                                                   (T_Env_16 -> Any
forall a b. a -> b
coe
                                                                      T_Env_16
MAlonzo.Code.Untyped.CEK.C_'91''93'_18)
                                                                   Any
v6))))
                                                       ((T_ExBudget_52 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                          T_ExBudget_52 -> Integer
MAlonzo.Code.Cost.d_ExMem_60
                                                          ((T_Writer_304 -> Any) -> Any -> Any
forall a b. a -> b
coe
                                                             T_Writer_304 -> Any
MAlonzo.Code.Utils.d_accum_316
                                                             ((T_MachineParameters_46 -> Integer -> T_State_218 -> T_Writer_304)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                T_MachineParameters_46 -> Integer -> T_State_218 -> T_Writer_304
MAlonzo.Code.Untyped.CEKWithCost.du_stepperC_338
                                                                ((T__'215'__364
   T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
 -> T_MachineParameters_46)
-> Any -> Any
forall a b. a -> b
coe
                                                                   T__'215'__364
  T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
-> T_MachineParameters_46
MAlonzo.Code.Cost.d_machineParameters_140
                                                                   ((Any -> Any -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                      Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378
                                                                      (Any -> Any
forall a b. a -> b
coe Any
v2) (Any -> Any
forall a b. a -> b
coe Any
v5)))
                                                                (Integer -> Any
forall a b. a -> b
coe
                                                                   Integer
MAlonzo.Code.Evaluator.Base.d_maxsteps_72)
                                                                ((T_Stack_6 -> T_Env_16 -> T__'8866'_14 -> T_State_218)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                   T_Stack_6 -> T_Env_16 -> T__'8866'_14 -> T_State_218
MAlonzo.Code.Untyped.CEK.C__'894'_'9659'__222
                                                                   (T_Stack_6 -> Any
forall a b. a -> b
coe
                                                                      T_Stack_6
MAlonzo.Code.Untyped.CEK.C_ε_10)
                                                                   (T_Env_16 -> Any
forall a b. a -> b
coe
                                                                      T_Env_16
MAlonzo.Code.Untyped.CEK.C_'91''93'_18)
                                                                   Any
v6))))))
                                          T_State_218
MAlonzo.Code.Untyped.CEK.C_'9670'_228
                                            -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                                                 Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                                                 ((RuntimeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                                                    RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20
                                                    (RuntimeError -> Any
forall a b. a -> b
coe RuntimeError
MAlonzo.Code.Utils.C_userError_352))
                                          T_State_218
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v8)))))
                Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
                  -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                       Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                       ((Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                          Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_jsonError_22
                          (Text -> Any
forall a b. a -> b
coe (Text
"while processing parameters." :: Data.Text.Text)))
                Maybe Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
      (Any, Any)
_ -> T_Either_6
  T_ERROR_12
  (T__'215'__364 T_TermU_24 (T__'215'__364 Integer Integer))
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Evaluator.Term.blah
blah ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
blah :: Text -> Text -> Text
blah = (Text -> Text -> Text) -> Text -> Text -> Text
forall a b. a -> b
coe Text -> Text -> Text
d_blah_240
d_blah_240 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_blah_240 :: Text -> Text -> Text
d_blah_240 Text
v0 Text
v1
  = let v2 :: t
v2 = (Text -> T_Either_6 T_ParseError_4 T_TermN_18) -> Text -> t
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TermN_18
d_parseTm_26 Text
v0 in
    Any -> Text
forall a b. a -> b
coe
      (let v3 :: t
v3 = (Text -> T_Either_6 T_ParseError_4 T_TermN_18) -> Text -> t
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TermN_18
d_parseTm_26 Text
v1 in
       Any -> Any
forall a b. a -> b
coe
         (case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v2 of
            MAlonzo.Code.Utils.C_inj'8322'_14 Any
v4
              -> case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v3 of
                   MAlonzo.Code.Utils.C_inj'8322'_14 Any
v5
                     -> let v6 :: t
v6 = (T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14) -> Any -> t
forall a b. a -> b
coe T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14
d_deBruijnifyTm_32 Any
v4 in
                        Any -> Any
forall a b. a -> b
coe
                          (let v7 :: t
v7 = (T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14) -> Any -> t
forall a b. a -> b
coe T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14
d_deBruijnifyTm_32 Any
v5 in
                           Any -> Any
forall a b. a -> b
coe
                             (case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v6 of
                                MAlonzo.Code.Utils.C_inj'8322'_14 Any
v8
                                  -> case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v7 of
                                       MAlonzo.Code.Utils.C_inj'8322'_14 Any
v9
                                         -> (Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                                              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                              (T_RawTm_30 -> Text
MAlonzo.Code.Raw.d_rawPrinter_344
                                                 ((T_Term_14 -> T_RawTm_30) -> Any -> T_RawTm_30
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 Any
v8))
                                              ((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
                                                 Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                 (Text
" || " :: Data.Text.Text)
                                                 (T_RawTm_30 -> Text
MAlonzo.Code.Raw.d_rawPrinter_344
                                                    ((T_Term_14 -> T_RawTm_30) -> Any -> T_RawTm_30
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 Any
v9)))
                                       T_Either_6 Any Any
_ -> Text -> Any
forall a b. a -> b
coe (Text
"deBruijnifying failed" :: Data.Text.Text)
                                T_Either_6 Any Any
_ -> Text -> Any
forall a b. a -> b
coe (Text
"deBruijnifying failed" :: Data.Text.Text)))
                   T_Either_6 Any Any
_ -> Text -> Any
forall a b. a -> b
coe (Text
"parsing failed" :: Data.Text.Text)
            T_Either_6 Any Any
_ -> Text -> Any
forall a b. a -> b
coe (Text
"parsing failed" :: Data.Text.Text)))
-- Evaluator.Term.printTy
printTy ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
printTy :: Text -> Text
printTy = (Text -> Text) -> Text -> Text
forall a b. a -> b
coe Text -> Text
d_printTy_286
d_printTy_286 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_printTy_286 :: Text -> Text
d_printTy_286 Text
v0
  = let v1 :: t
v1 = (Text -> T_Either_6 T_ParseError_4 T_TypeN_20) -> Text -> t
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TypeN_20
d_parseTy_30 Text
v0 in
    Any -> Text
forall a b. a -> b
coe
      (case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v1 of
         MAlonzo.Code.Utils.C_inj'8321'_12 Any
v2
           -> Text -> Any
forall a b. a -> b
coe (Text
"parseTy error" :: Data.Text.Text)
         MAlonzo.Code.Utils.C_inj'8322'_14 Any
v2
           -> let v3 :: t
v3 = (T_TypeN_20 -> T_Either_6 FreeVariableError T_Type_16) -> Any -> t
forall a b. a -> b
coe T_TypeN_20 -> T_Either_6 FreeVariableError T_Type_16
d_deBruijnifyTy_34 Any
v2 in
              Any -> Any
forall a b. a -> b
coe
                (case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v3 of
                   MAlonzo.Code.Utils.C_inj'8321'_12 Any
v4
                     -> Text -> Any
forall a b. a -> b
coe (Text
"deBruinjifyTy error" :: Data.Text.Text)
                   MAlonzo.Code.Utils.C_inj'8322'_14 Any
v4
                     -> (T_RawTy_2 -> Text) -> Any -> Any
forall a b. a -> b
coe T_RawTy_2 -> Text
MAlonzo.Code.Raw.d_rawTyPrinter_294 ((T_Type_16 -> T_RawTy_2) -> Any -> Any
forall a b. a -> b
coe T_Type_16 -> T_RawTy_2
d_convTy_42 Any
v4)
                   T_Either_6 Any Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
         T_Either_6 Any Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Evaluator.Term.alphaTy
alphaTy ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 -> Bool
alphaTy :: Text -> Text -> Bool
alphaTy = (Text -> Text -> Bool) -> Text -> Text -> Bool
forall a b. a -> b
coe Text -> Text -> Bool
d_alphaTy_314
d_alphaTy_314 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 -> Bool
d_alphaTy_314 :: Text -> Text -> Bool
d_alphaTy_314 Text
v0 Text
v1
  = let v2 :: t
v2 = (Text -> T_Either_6 T_ParseError_4 T_TypeN_20) -> Text -> t
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TypeN_20
d_parseTy_30 Text
v0 in
    Any -> Bool
forall a b. a -> b
coe
      (let v3 :: t
v3 = (Text -> T_Either_6 T_ParseError_4 T_TypeN_20) -> Text -> t
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TypeN_20
d_parseTy_30 Text
v1 in
       Any -> Any
forall a b. a -> b
coe
         (case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v2 of
            MAlonzo.Code.Utils.C_inj'8322'_14 Any
v4
              -> case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v3 of
                   MAlonzo.Code.Utils.C_inj'8322'_14 Any
v5
                     -> let v6 :: t
v6 = (T_TypeN_20 -> T_Either_6 FreeVariableError T_Type_16) -> Any -> t
forall a b. a -> b
coe T_TypeN_20 -> T_Either_6 FreeVariableError T_Type_16
d_deBruijnifyTy_34 Any
v4 in
                        Any -> Any
forall a b. a -> b
coe
                          (let v7 :: t
v7 = (T_TypeN_20 -> T_Either_6 FreeVariableError T_Type_16) -> Any -> t
forall a b. a -> b
coe T_TypeN_20 -> T_Either_6 FreeVariableError T_Type_16
d_deBruijnifyTy_34 Any
v5 in
                           Any -> Any
forall a b. a -> b
coe
                             (case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v6 of
                                MAlonzo.Code.Utils.C_inj'8322'_14 Any
v8
                                  -> case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v7 of
                                       MAlonzo.Code.Utils.C_inj'8322'_14 Any
v9
                                         -> (T_RawTy_2 -> T_RawTy_2 -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
                                              T_RawTy_2 -> T_RawTy_2 -> Bool
MAlonzo.Code.Raw.d_decRTy_100 ((T_Type_16 -> T_RawTy_2) -> Any -> Any
forall a b. a -> b
coe T_Type_16 -> T_RawTy_2
d_convTy_42 Any
v8)
                                              ((T_Type_16 -> T_RawTy_2) -> Any -> Any
forall a b. a -> b
coe T_Type_16 -> T_RawTy_2
d_convTy_42 Any
v9)
                                       T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
                                T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
                   T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
            T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
-- Evaluator.Term.alphaTm
alphaTm ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 -> Bool
alphaTm :: Text -> Text -> Bool
alphaTm = (Text -> Text -> Bool) -> Text -> Text -> Bool
forall a b. a -> b
coe Text -> Text -> Bool
d_alphaTm_360
d_alphaTm_360 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 -> Bool
d_alphaTm_360 :: Text -> Text -> Bool
d_alphaTm_360 Text
v0 Text
v1
  = let v2 :: t
v2 = (Text -> T_Either_6 T_ParseError_4 T_TermN_18) -> Text -> t
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TermN_18
d_parseTm_26 Text
v0 in
    Any -> Bool
forall a b. a -> b
coe
      (let v3 :: t
v3 = (Text -> T_Either_6 T_ParseError_4 T_TermN_18) -> Text -> t
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TermN_18
d_parseTm_26 Text
v1 in
       Any -> Any
forall a b. a -> b
coe
         (case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v2 of
            MAlonzo.Code.Utils.C_inj'8322'_14 Any
v4
              -> case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v3 of
                   MAlonzo.Code.Utils.C_inj'8322'_14 Any
v5
                     -> let v6 :: t
v6 = (T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14) -> Any -> t
forall a b. a -> b
coe T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14
d_deBruijnifyTm_32 Any
v4 in
                        Any -> Any
forall a b. a -> b
coe
                          (let v7 :: t
v7 = (T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14) -> Any -> t
forall a b. a -> b
coe T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14
d_deBruijnifyTm_32 Any
v5 in
                           Any -> Any
forall a b. a -> b
coe
                             (case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v6 of
                                MAlonzo.Code.Utils.C_inj'8322'_14 Any
v8
                                  -> case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v7 of
                                       MAlonzo.Code.Utils.C_inj'8322'_14 Any
v9
                                         -> (T_RawTm_30 -> T_RawTm_30 -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
                                              T_RawTm_30 -> T_RawTm_30 -> Bool
MAlonzo.Code.Raw.d_decRTm_186 ((T_Term_14 -> T_RawTm_30) -> Any -> Any
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 Any
v8)
                                              ((T_Term_14 -> T_RawTm_30) -> Any -> Any
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 Any
v9)
                                       T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
                                T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
                   T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
            T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
-- Evaluator.Term.alphaU
alphaU ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 -> Bool
alphaU :: Text -> Text -> Bool
alphaU = (Text -> Text -> Bool) -> Text -> Text -> Bool
forall a b. a -> b
coe Text -> Text -> Bool
d_alphaU_406
d_alphaU_406 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 -> Bool
d_alphaU_406 :: Text -> Text -> Bool
d_alphaU_406 Text
v0 Text
v1
  = let v2 :: t
v2 = (Text -> T_Either_6 T_ParseError_4 T_TermNU_22) -> Text -> t
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TermNU_22
d_parseTmU_28 Text
v0 in
    Any -> Bool
forall a b. a -> b
coe
      (let v3 :: t
v3 = (Text -> T_Either_6 T_ParseError_4 T_TermNU_22) -> Text -> t
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TermNU_22
d_parseTmU_28 Text
v1 in
       Any -> Any
forall a b. a -> b
coe
         (case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v2 of
            MAlonzo.Code.Utils.C_inj'8322'_14 Any
v4
              -> case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v3 of
                   MAlonzo.Code.Utils.C_inj'8322'_14 Any
v5
                     -> let v6 :: t
v6 = (T_TermNU_22 -> T_Either_6 FreeVariableError T_TermU_24)
-> Any -> t
forall a b. a -> b
coe T_TermNU_22 -> T_Either_6 FreeVariableError T_TermU_24
d_deBruijnifyTmU_36 Any
v4 in
                        Any -> Any
forall a b. a -> b
coe
                          (let v7 :: t
v7 = (T_TermNU_22 -> T_Either_6 FreeVariableError T_TermU_24)
-> Any -> t
forall a b. a -> b
coe T_TermNU_22 -> T_Either_6 FreeVariableError T_TermU_24
d_deBruijnifyTmU_36 Any
v5 in
                           Any -> Any
forall a b. a -> b
coe
                             (case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v6 of
                                MAlonzo.Code.Utils.C_inj'8322'_14 Any
v8
                                  -> case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall a. a
v7 of
                                       MAlonzo.Code.Utils.C_inj'8322'_14 Any
v9
                                         -> (T_Untyped_146 -> T_Untyped_146 -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
                                              T_Untyped_146 -> T_Untyped_146 -> Bool
MAlonzo.Code.Untyped.d_decUTm_314
                                              ((T_TermU_24 -> T_Untyped_146) -> Any -> Any
forall a b. a -> b
coe T_TermU_24 -> T_Untyped_146
d_convTmU_46 Any
v8) ((T_TermU_24 -> T_Untyped_146) -> Any -> Any
forall a b. a -> b
coe T_TermU_24 -> T_Untyped_146
d_convTmU_46 Any
v9)
                                       T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
                                T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
                   T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
            T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))