{-# 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.Scoped where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Nat
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Builtin.Constant.AtomicType
import qualified MAlonzo.Code.Builtin.Constant.Type
import qualified MAlonzo.Code.Builtin.Signature
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.Data.Integer.Show
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.Raw
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Utils

import PlutusCore.DeBruijn
import Raw
import qualified Data.Text as T
-- Scoped.ScopedTy
d_ScopedTy_14 :: p -> ()
d_ScopedTy_14 p
a0 = ()
data T_ScopedTy_14
  = C_'96'_18 MAlonzo.Code.Data.Fin.Base.T_Fin_6 |
    C__'8658'__20 T_ScopedTy_14 T_ScopedTy_14 |
    C_Π_22 MAlonzo.Code.Utils.T_Kind_476 T_ScopedTy_14 |
    C_ƛ_24 MAlonzo.Code.Utils.T_Kind_476 T_ScopedTy_14 |
    C__'183'__26 T_ScopedTy_14 T_ScopedTy_14 |
    C_con_30 MAlonzo.Code.Utils.T_Kind_476
             MAlonzo.Code.Builtin.Constant.Type.T_TyCon_6 |
    C_μ_32 T_ScopedTy_14 T_ScopedTy_14 |
    C_SOP_34 (MAlonzo.Code.Utils.T_List_382
                (MAlonzo.Code.Utils.T_List_382 T_ScopedTy_14))
-- Scoped.Tel⋆
d_Tel'8902'_36 :: Integer -> Integer -> ()
d_Tel'8902'_36 :: Integer -> Integer -> ()
d_Tel'8902'_36 = Integer -> Integer -> ()
forall a. a
erased
-- Scoped.Weirdℕ
d_Weirdℕ_42 :: p -> ()
d_Weirdℕ_42 p
a0 = ()
data T_Weirdℕ_42 = C_Z_44 | C_S_48 T_Weirdℕ_42 | C_T_52 T_Weirdℕ_42
-- Scoped.WeirdFin
d_WeirdFin_56 :: p -> p -> ()
d_WeirdFin_56 p
a0 p
a1 = ()
data T_WeirdFin_56
  = C_Z_62 | C_S_68 T_WeirdFin_56 | C_T_74 T_WeirdFin_56
-- Scoped.wtoℕ
d_wtoℕ_78 :: Integer -> T_Weirdℕ_42 -> Integer
d_wtoℕ_78 :: Integer -> T_Weirdℕ_42 -> Integer
d_wtoℕ_78 ~Integer
v0 T_Weirdℕ_42
v1 = T_Weirdℕ_42 -> Integer
du_wtoℕ_78 T_Weirdℕ_42
v1
du_wtoℕ_78 :: T_Weirdℕ_42 -> Integer
du_wtoℕ_78 :: T_Weirdℕ_42 -> Integer
du_wtoℕ_78 T_Weirdℕ_42
v0
  = case T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
v0 of
      T_Weirdℕ_42
C_Z_44 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      C_S_48 T_Weirdℕ_42
v2
        -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) ((T_Weirdℕ_42 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> Integer
du_wtoℕ_78 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v2))
      C_T_52 T_Weirdℕ_42
v2
        -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) ((T_Weirdℕ_42 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> Integer
du_wtoℕ_78 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v2))
      T_Weirdℕ_42
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.WeirdFintoℕ
d_WeirdFintoℕ_88 ::
  Integer -> T_Weirdℕ_42 -> T_WeirdFin_56 -> Integer
d_WeirdFintoℕ_88 :: Integer -> T_Weirdℕ_42 -> T_WeirdFin_56 -> Integer
d_WeirdFintoℕ_88 ~Integer
v0 T_Weirdℕ_42
v1 T_WeirdFin_56
v2 = T_Weirdℕ_42 -> T_WeirdFin_56 -> Integer
du_WeirdFintoℕ_88 T_Weirdℕ_42
v1 T_WeirdFin_56
v2
du_WeirdFintoℕ_88 :: T_Weirdℕ_42 -> T_WeirdFin_56 -> Integer
du_WeirdFintoℕ_88 :: T_Weirdℕ_42 -> T_WeirdFin_56 -> Integer
du_WeirdFintoℕ_88 T_Weirdℕ_42
v0 T_WeirdFin_56
v1
  = case T_WeirdFin_56 -> T_WeirdFin_56
forall a b. a -> b
coe T_WeirdFin_56
v1 of
      T_WeirdFin_56
C_Z_62 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      C_S_68 T_WeirdFin_56
v4
        -> case T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
v0 of
             C_S_48 T_Weirdℕ_42
v6
               -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
                    Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                    ((T_Weirdℕ_42 -> T_WeirdFin_56 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_WeirdFin_56 -> Integer
du_WeirdFintoℕ_88 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v6) (T_WeirdFin_56 -> Any
forall a b. a -> b
coe T_WeirdFin_56
v4))
             T_Weirdℕ_42
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_T_74 T_WeirdFin_56
v4
        -> case T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
v0 of
             C_T_52 T_Weirdℕ_42
v6 -> (T_Weirdℕ_42 -> T_WeirdFin_56 -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe T_Weirdℕ_42 -> T_WeirdFin_56 -> Integer
du_WeirdFintoℕ_88 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v6) (T_WeirdFin_56 -> Any
forall a b. a -> b
coe T_WeirdFin_56
v4)
             T_Weirdℕ_42
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_WeirdFin_56
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.wtoℕTm
d_wtoℕTm_96 :: Integer -> T_Weirdℕ_42 -> Integer
d_wtoℕTm_96 :: Integer -> T_Weirdℕ_42 -> Integer
d_wtoℕTm_96 ~Integer
v0 T_Weirdℕ_42
v1 = T_Weirdℕ_42 -> Integer
du_wtoℕTm_96 T_Weirdℕ_42
v1
du_wtoℕTm_96 :: T_Weirdℕ_42 -> Integer
du_wtoℕTm_96 :: T_Weirdℕ_42 -> Integer
du_wtoℕTm_96 T_Weirdℕ_42
v0
  = case T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
v0 of
      T_Weirdℕ_42
C_Z_44 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      C_S_48 T_Weirdℕ_42
v2
        -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) ((T_Weirdℕ_42 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> Integer
du_wtoℕTm_96 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v2))
      C_T_52 T_Weirdℕ_42
v2 -> (T_Weirdℕ_42 -> Integer) -> Any -> Integer
forall a b. a -> b
coe T_Weirdℕ_42 -> Integer
du_wtoℕTm_96 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v2)
      T_Weirdℕ_42
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.wtoℕTy
d_wtoℕTy_104 :: Integer -> T_Weirdℕ_42 -> Integer
d_wtoℕTy_104 :: Integer -> T_Weirdℕ_42 -> Integer
d_wtoℕTy_104 ~Integer
v0 T_Weirdℕ_42
v1 = T_Weirdℕ_42 -> Integer
du_wtoℕTy_104 T_Weirdℕ_42
v1
du_wtoℕTy_104 :: T_Weirdℕ_42 -> Integer
du_wtoℕTy_104 :: T_Weirdℕ_42 -> Integer
du_wtoℕTy_104 T_Weirdℕ_42
v0
  = case T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
v0 of
      T_Weirdℕ_42
C_Z_44 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      C_S_48 T_Weirdℕ_42
v2 -> (T_Weirdℕ_42 -> Integer) -> Any -> Integer
forall a b. a -> b
coe T_Weirdℕ_42 -> Integer
du_wtoℕTm_96 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v2)
      C_T_52 T_Weirdℕ_42
v2
        -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) ((T_Weirdℕ_42 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> Integer
du_wtoℕTm_96 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v2))
      T_Weirdℕ_42
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.lookupWTm
d_lookupWTm_116 ::
  Integer -> Integer -> T_Weirdℕ_42 -> Maybe Integer
d_lookupWTm_116 :: Integer -> Integer -> T_Weirdℕ_42 -> Maybe Integer
d_lookupWTm_116 Integer
v0 ~Integer
v1 T_Weirdℕ_42
v2 = Integer -> T_Weirdℕ_42 -> Maybe Integer
du_lookupWTm_116 Integer
v0 T_Weirdℕ_42
v2
du_lookupWTm_116 :: Integer -> T_Weirdℕ_42 -> Maybe Integer
du_lookupWTm_116 :: Integer -> T_Weirdℕ_42 -> Maybe Integer
du_lookupWTm_116 Integer
v0 T_Weirdℕ_42
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> case T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
v1 of
             T_Weirdℕ_42
C_Z_44 -> Maybe Any -> Maybe Integer
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
             C_S_48 T_Weirdℕ_42
v3
               -> (Any -> Maybe Any) -> Any -> Maybe Integer
forall a b. a -> b
coe
                    Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
             C_T_52 T_Weirdℕ_42
v3 -> Maybe Any -> Maybe Integer
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
             T_Weirdℕ_42
_ -> Maybe Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> Maybe Integer
forall a b. a -> b
coe
             (case T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
v1 of
                T_Weirdℕ_42
C_Z_44 -> Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
                C_S_48 T_Weirdℕ_42
v4
                  -> (T_Monad_186 -> (Any -> Any) -> Any -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Monad_186 -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Utils.du_fmap_224
                       (T_Monad_186 -> Any
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.d_MaybeMonad_240)
                       ((Any -> Integer) -> Any
forall a b. a -> b
coe (\ Any
v5 -> Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Any -> Integer
forall a b. a -> b
coe Any
v5)))
                       ((Integer -> T_Weirdℕ_42 -> Maybe Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> Maybe Integer
du_lookupWTm_116 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v4))
                C_T_52 T_Weirdℕ_42
v4 -> (Integer -> T_Weirdℕ_42 -> Maybe Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> Maybe Integer
du_lookupWTm_116 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v4)
                T_Weirdℕ_42
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Scoped.lookupWTy
d_lookupWTy_138 ::
  Integer -> Integer -> T_Weirdℕ_42 -> Maybe Integer
d_lookupWTy_138 :: Integer -> Integer -> T_Weirdℕ_42 -> Maybe Integer
d_lookupWTy_138 Integer
v0 ~Integer
v1 T_Weirdℕ_42
v2 = Integer -> T_Weirdℕ_42 -> Maybe Integer
du_lookupWTy_138 Integer
v0 T_Weirdℕ_42
v2
du_lookupWTy_138 :: Integer -> T_Weirdℕ_42 -> Maybe Integer
du_lookupWTy_138 :: Integer -> T_Weirdℕ_42 -> Maybe Integer
du_lookupWTy_138 Integer
v0 T_Weirdℕ_42
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> case T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
v1 of
             T_Weirdℕ_42
C_Z_44 -> Maybe Any -> Maybe Integer
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
             C_S_48 T_Weirdℕ_42
v3 -> Maybe Any -> Maybe Integer
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
             C_T_52 T_Weirdℕ_42
v3
               -> (Any -> Maybe Any) -> Any -> Maybe Integer
forall a b. a -> b
coe
                    Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
             T_Weirdℕ_42
_ -> Maybe Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> Maybe Integer
forall a b. a -> b
coe
             (case T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
v1 of
                T_Weirdℕ_42
C_Z_44 -> Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
                C_S_48 T_Weirdℕ_42
v4 -> (Integer -> T_Weirdℕ_42 -> Maybe Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> Maybe Integer
du_lookupWTy_138 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v4)
                C_T_52 T_Weirdℕ_42
v4
                  -> (T_Monad_186 -> (Any -> Any) -> Any -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Monad_186 -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Utils.du_fmap_224
                       (T_Monad_186 -> Any
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.d_MaybeMonad_240)
                       ((Any -> Integer) -> Any
forall a b. a -> b
coe (\ Any
v5 -> Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Any -> Integer
forall a b. a -> b
coe Any
v5)))
                       ((Integer -> T_Weirdℕ_42 -> Maybe Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> Maybe Integer
du_lookupWTy_138 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v4))
                T_Weirdℕ_42
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Scoped.lookupWTm'
d_lookupWTm''_158 :: Integer -> Integer -> T_Weirdℕ_42 -> Integer
d_lookupWTm''_158 :: Integer -> Integer -> T_Weirdℕ_42 -> Integer
d_lookupWTm''_158 Integer
v0 ~Integer
v1 T_Weirdℕ_42
v2 = Integer -> T_Weirdℕ_42 -> Integer
du_lookupWTm''_158 Integer
v0 T_Weirdℕ_42
v2
du_lookupWTm''_158 :: Integer -> T_Weirdℕ_42 -> Integer
du_lookupWTm''_158 :: Integer -> T_Weirdℕ_42 -> Integer
du_lookupWTm''_158 Integer
v0 T_Weirdℕ_42
v1
  = case T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
v1 of
      T_Weirdℕ_42
C_Z_44 -> Integer -> Integer
forall a b. a -> b
coe Integer
v0
      C_S_48 T_Weirdℕ_42
v3
        -> case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
             Integer
0 -> Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)
             Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                  Any -> Integer
forall a b. a -> b
coe
                    ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                       Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                       ((Integer -> T_Weirdℕ_42 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> Integer
du_lookupWTm''_158 (Integer -> Any
forall a b. a -> b
coe Integer
v4) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v3)))
      C_T_52 T_Weirdℕ_42
v3
        -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
             Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
             ((Integer -> T_Weirdℕ_42 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> Integer
du_lookupWTm''_158 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v3))
      T_Weirdℕ_42
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.lookupWTy'
d_lookupWTy''_176 :: Integer -> Integer -> T_Weirdℕ_42 -> Integer
d_lookupWTy''_176 :: Integer -> Integer -> T_Weirdℕ_42 -> Integer
d_lookupWTy''_176 Integer
v0 ~Integer
v1 T_Weirdℕ_42
v2 = Integer -> T_Weirdℕ_42 -> Integer
du_lookupWTy''_176 Integer
v0 T_Weirdℕ_42
v2
du_lookupWTy''_176 :: Integer -> T_Weirdℕ_42 -> Integer
du_lookupWTy''_176 :: Integer -> T_Weirdℕ_42 -> Integer
du_lookupWTy''_176 Integer
v0 T_Weirdℕ_42
v1
  = case T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
v1 of
      T_Weirdℕ_42
C_Z_44 -> Integer -> Integer
forall a b. a -> b
coe Integer
v0
      C_S_48 T_Weirdℕ_42
v3
        -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
             Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
             ((Integer -> T_Weirdℕ_42 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> Integer
du_lookupWTy''_176 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v3))
      C_T_52 T_Weirdℕ_42
v3
        -> case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
             Integer
0 -> Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)
             Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                  Any -> Integer
forall a b. a -> b
coe
                    ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                       Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                       ((Integer -> T_Weirdℕ_42 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> Integer
du_lookupWTy''_176 (Integer -> Any
forall a b. a -> b
coe Integer
v4) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v3)))
      T_Weirdℕ_42
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.shifterTy
d_shifterTy_194 ::
  Integer ->
  T_Weirdℕ_42 ->
  MAlonzo.Code.Raw.T_RawTy_2 -> MAlonzo.Code.Raw.T_RawTy_2
d_shifterTy_194 :: Integer -> T_Weirdℕ_42 -> T_RawTy_2 -> T_RawTy_2
d_shifterTy_194 Integer
v0 T_Weirdℕ_42
v1 T_RawTy_2
v2
  = case T_RawTy_2 -> T_RawTy_2
forall a b. a -> b
coe T_RawTy_2
v2 of
      MAlonzo.Code.Raw.C_'96'_6 Integer
v3
        -> (Integer -> T_RawTy_2) -> Any -> T_RawTy_2
forall a b. a -> b
coe
             Integer -> T_RawTy_2
MAlonzo.Code.Raw.C_'96'_6
             (((Any -> Any) -> Any -> Maybe Any -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                (Any -> Any) -> Any -> Maybe Any -> Any
MAlonzo.Code.Data.Maybe.Base.du_maybe_36 ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v4 -> Any
v4))
                (Integer -> Any
forall a b. a -> b
coe (Integer
100 :: Integer))
                ((Integer -> T_Weirdℕ_42 -> Maybe Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                   Integer -> T_Weirdℕ_42 -> Maybe Integer
du_lookupWTy_138
                   ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                      Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d_'8739'_'45'_'8739'_142 (Integer -> Any
forall a b. a -> b
coe Integer
v3)
                      (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)))
                   (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1)))
      MAlonzo.Code.Raw.C__'8658'__8 T_RawTy_2
v3 T_RawTy_2
v4
        -> (T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Raw.C__'8658'__8
             ((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
d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
             ((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
d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v4))
      MAlonzo.Code.Raw.C_Π_10 KIND
v3 T_RawTy_2
v4
        -> (KIND -> T_RawTy_2 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
             KIND -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Raw.C_Π_10 (KIND -> Any
forall a b. a -> b
coe KIND
v3)
             ((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
d_shifterTy_194 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                ((T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
C_T_52 T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v4))
      MAlonzo.Code.Raw.C_ƛ_12 KIND
v3 T_RawTy_2
v4
        -> (KIND -> T_RawTy_2 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
             KIND -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Raw.C_ƛ_12 (KIND -> Any
forall a b. a -> b
coe KIND
v3)
             ((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
d_shifterTy_194 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                ((T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
C_T_52 T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v4))
      MAlonzo.Code.Raw.C__'183'__14 T_RawTy_2
v3 T_RawTy_2
v4
        -> (T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Raw.C__'183'__14
             ((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
d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
             ((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
d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v4))
      MAlonzo.Code.Raw.C_con_16 RTyCon
v3 -> T_RawTy_2 -> T_RawTy_2
forall a b. a -> b
coe T_RawTy_2
v2
      MAlonzo.Code.Raw.C_μ_18 T_RawTy_2
v3 T_RawTy_2
v4
        -> (T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Raw.C_μ_18
             ((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
d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
             ((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
d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v4))
      MAlonzo.Code.Raw.C_SOP_22 [[T_RawTy_2]]
v3
        -> ([[T_RawTy_2]] -> T_RawTy_2) -> Any -> T_RawTy_2
forall a b. a -> b
coe
             [[T_RawTy_2]] -> T_RawTy_2
MAlonzo.Code.Raw.C_SOP_22
             ((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]]
d_shifterTyListList_206 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) ([[T_RawTy_2]] -> Any
forall a b. a -> b
coe [[T_RawTy_2]]
v3))
      T_RawTy_2
_ -> T_RawTy_2
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.shifterTyList
d_shifterTyList_200 ::
  Integer ->
  T_Weirdℕ_42 ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTy_2 ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTy_2
d_shifterTyList_200 :: Integer -> T_Weirdℕ_42 -> [T_RawTy_2] -> [T_RawTy_2]
d_shifterTyList_200 Integer
v0 T_Weirdℕ_42
v1 [T_RawTy_2]
v2
  = case [T_RawTy_2] -> [Any]
forall a b. a -> b
coe [T_RawTy_2]
v2 of
      [Any]
MAlonzo.Code.Utils.C_'91''93'_386 -> [T_RawTy_2] -> [T_RawTy_2]
forall a b. a -> b
coe [T_RawTy_2]
v2
      MAlonzo.Code.Utils.C__'8759'__388 Any
v3 [Any]
v4
        -> (Any -> [Any] -> [Any]) -> Any -> Any -> [T_RawTy_2]
forall a b. a -> b
coe
             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
             ((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
d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (Any -> Any
forall a b. a -> b
coe Any
v3))
             ((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]
d_shifterTyList_200 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) ([Any] -> Any
forall a b. a -> b
coe [Any]
v4))
      [Any]
_ -> [T_RawTy_2]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.shifterTyListList
d_shifterTyListList_206 ::
  Integer ->
  T_Weirdℕ_42 ->
  MAlonzo.Code.Utils.T_List_382
    (MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTy_2) ->
  MAlonzo.Code.Utils.T_List_382
    (MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTy_2)
d_shifterTyListList_206 :: Integer -> T_Weirdℕ_42 -> [[T_RawTy_2]] -> [[T_RawTy_2]]
d_shifterTyListList_206 Integer
v0 T_Weirdℕ_42
v1 [[T_RawTy_2]]
v2
  = case [[T_RawTy_2]] -> [Any]
forall a b. a -> b
coe [[T_RawTy_2]]
v2 of
      [Any]
MAlonzo.Code.Utils.C_'91''93'_386 -> [[T_RawTy_2]] -> [[T_RawTy_2]]
forall a b. a -> b
coe [[T_RawTy_2]]
v2
      MAlonzo.Code.Utils.C__'8759'__388 Any
v3 [Any]
v4
        -> (Any -> [Any] -> [Any]) -> Any -> Any -> [[T_RawTy_2]]
forall a b. a -> b
coe
             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
             ((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]
d_shifterTyList_200 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (Any -> Any
forall a b. a -> b
coe Any
v3))
             ((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]]
d_shifterTyListList_206 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) ([Any] -> Any
forall a b. a -> b
coe [Any]
v4))
      [Any]
_ -> [[T_RawTy_2]]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.shifter
d_shifter_272 ::
  Integer ->
  T_Weirdℕ_42 ->
  MAlonzo.Code.Raw.T_RawTm_30 -> MAlonzo.Code.Raw.T_RawTm_30
d_shifter_272 :: Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
d_shifter_272 Integer
v0 T_Weirdℕ_42
v1 T_RawTm_30
v2
  = case T_RawTm_30 -> T_RawTm_30
forall a b. a -> b
coe T_RawTm_30
v2 of
      MAlonzo.Code.Raw.C_'96'_32 Integer
v3
        -> (Integer -> T_RawTm_30) -> Any -> T_RawTm_30
forall a b. a -> b
coe
             Integer -> T_RawTm_30
MAlonzo.Code.Raw.C_'96'_32
             (((Any -> Any) -> Any -> Maybe Any -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                (Any -> Any) -> Any -> Maybe Any -> Any
MAlonzo.Code.Data.Maybe.Base.du_maybe_36 ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v4 -> Any
v4))
                (Integer -> Any
forall a b. a -> b
coe (Integer
100 :: Integer))
                ((Integer -> T_Weirdℕ_42 -> Maybe Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                   Integer -> T_Weirdℕ_42 -> Maybe Integer
du_lookupWTm_116
                   ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                      Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d_'8739'_'45'_'8739'_142 (Integer -> Any
forall a b. a -> b
coe Integer
v3)
                      (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)))
                   (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1)))
      MAlonzo.Code.Raw.C_Λ_34 KIND
v3 T_RawTm_30
v4
        -> (KIND -> T_RawTm_30 -> T_RawTm_30) -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             KIND -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Raw.C_Λ_34 (KIND -> Any
forall a b. a -> b
coe KIND
v3)
             ((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
d_shifter_272 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                ((T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
C_T_52 T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v4))
      MAlonzo.Code.Raw.C__'183''8902'__36 T_RawTm_30
v3 T_RawTy_2
v4
        -> (T_RawTm_30 -> T_RawTy_2 -> T_RawTm_30) -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTm_30 -> T_RawTy_2 -> T_RawTm_30
MAlonzo.Code.Raw.C__'183''8902'__36
             ((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
d_shifter_272 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v3))
             ((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
d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v4))
      MAlonzo.Code.Raw.C_ƛ_38 T_RawTy_2
v3 T_RawTm_30
v4
        -> (T_RawTy_2 -> T_RawTm_30 -> T_RawTm_30) -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Raw.C_ƛ_38
             ((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
d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ((T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
C_S_48 T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
             ((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
d_shifter_272 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ((T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
C_S_48 T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v4))
      MAlonzo.Code.Raw.C__'183'__40 T_RawTm_30
v3 T_RawTm_30
v4
        -> (T_RawTm_30 -> T_RawTm_30 -> T_RawTm_30)
-> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTm_30 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Raw.C__'183'__40
             ((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
d_shifter_272 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v3))
             ((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
d_shifter_272 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v4))
      MAlonzo.Code.Raw.C_con_42 Some (ValueOf DefaultUni)
v3 -> T_RawTm_30 -> T_RawTm_30
forall a b. a -> b
coe T_RawTm_30
v2
      MAlonzo.Code.Raw.C_error_44 T_RawTy_2
v3
        -> (T_RawTy_2 -> T_RawTm_30) -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTm_30
MAlonzo.Code.Raw.C_error_44
             ((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
d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
      MAlonzo.Code.Raw.C_builtin_46 DefaultFun
v3 -> T_RawTm_30 -> T_RawTm_30
forall a b. a -> b
coe T_RawTm_30
v2
      MAlonzo.Code.Raw.C_wrap_48 T_RawTy_2
v3 T_RawTy_2
v4 T_RawTm_30
v5
        -> (T_RawTy_2 -> T_RawTy_2 -> T_RawTm_30 -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTy_2 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Raw.C_wrap_48
             ((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
d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
             ((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
d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v4))
             ((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
d_shifter_272 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v5))
      MAlonzo.Code.Raw.C_unwrap_50 T_RawTm_30
v3
        -> (T_RawTm_30 -> T_RawTm_30) -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Raw.C_unwrap_50
             ((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
d_shifter_272 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v3))
      MAlonzo.Code.Raw.C_constr_58 T_RawTy_2
v3 Integer
v4 [T_RawTm_30]
v5
        -> (T_RawTy_2 -> Integer -> [T_RawTm_30] -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTy_2 -> Integer -> [T_RawTm_30] -> T_RawTm_30
MAlonzo.Code.Raw.C_constr_58
             ((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
d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3)) (Integer -> Any
forall a b. a -> b
coe Integer
v4)
             ((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]
d_shifterList_278 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) ([T_RawTm_30] -> Any
forall a b. a -> b
coe [T_RawTm_30]
v5))
      MAlonzo.Code.Raw.C_case_66 T_RawTy_2
v3 T_RawTm_30
v4 [T_RawTm_30]
v5
        -> (T_RawTy_2 -> T_RawTm_30 -> [T_RawTm_30] -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTm_30 -> [T_RawTm_30] -> T_RawTm_30
MAlonzo.Code.Raw.C_case_66
             ((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
d_shifterTy_194 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
             ((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
d_shifter_272 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v4))
             ((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]
d_shifterList_278 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) ([T_RawTm_30] -> Any
forall a b. a -> b
coe [T_RawTm_30]
v5))
      T_RawTm_30
_ -> T_RawTm_30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.shifterList
d_shifterList_278 ::
  Integer ->
  T_Weirdℕ_42 ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTm_30 ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTm_30
d_shifterList_278 :: Integer -> T_Weirdℕ_42 -> [T_RawTm_30] -> [T_RawTm_30]
d_shifterList_278 Integer
v0 T_Weirdℕ_42
v1 [T_RawTm_30]
v2
  = case [T_RawTm_30] -> [Any]
forall a b. a -> b
coe [T_RawTm_30]
v2 of
      [Any]
MAlonzo.Code.Utils.C_'91''93'_386 -> [T_RawTm_30] -> [T_RawTm_30]
forall a b. a -> b
coe [T_RawTm_30]
v2
      MAlonzo.Code.Utils.C__'8759'__388 Any
v3 [Any]
v4
        -> (Any -> [Any] -> [Any]) -> Any -> Any -> [T_RawTm_30]
forall a b. a -> b
coe
             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
             ((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
d_shifter_272 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (Any -> Any
forall a b. a -> b
coe Any
v3))
             ((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]
d_shifterList_278 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) ([Any] -> Any
forall a b. a -> b
coe [Any]
v4))
      [Any]
_ -> [T_RawTm_30]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.unshifterTy
d_unshifterTy_360 ::
  Integer ->
  T_Weirdℕ_42 ->
  MAlonzo.Code.Raw.T_RawTy_2 -> MAlonzo.Code.Raw.T_RawTy_2
d_unshifterTy_360 :: Integer -> T_Weirdℕ_42 -> T_RawTy_2 -> T_RawTy_2
d_unshifterTy_360 Integer
v0 T_Weirdℕ_42
v1 T_RawTy_2
v2
  = case T_RawTy_2 -> T_RawTy_2
forall a b. a -> b
coe T_RawTy_2
v2 of
      MAlonzo.Code.Raw.C_'96'_6 Integer
v3
        -> (Integer -> T_RawTy_2) -> Any -> T_RawTy_2
forall a b. a -> b
coe
             Integer -> T_RawTy_2
MAlonzo.Code.Raw.C_'96'_6
             ((Integer -> T_Weirdℕ_42 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> Integer
du_lookupWTy''_176 (Integer -> Any
forall a b. a -> b
coe Integer
v3) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1))
      MAlonzo.Code.Raw.C__'8658'__8 T_RawTy_2
v3 T_RawTy_2
v4
        -> (T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Raw.C__'8658'__8
             ((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
d_unshifterTy_360 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
             ((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
d_unshifterTy_360 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v4))
      MAlonzo.Code.Raw.C_Π_10 KIND
v3 T_RawTy_2
v4
        -> (KIND -> T_RawTy_2 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
             KIND -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Raw.C_Π_10 (KIND -> Any
forall a b. a -> b
coe KIND
v3)
             ((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
d_unshifterTy_360 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                ((T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
C_T_52 T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v4))
      MAlonzo.Code.Raw.C_ƛ_12 KIND
v3 T_RawTy_2
v4
        -> (KIND -> T_RawTy_2 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
             KIND -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Raw.C_ƛ_12 (KIND -> Any
forall a b. a -> b
coe KIND
v3)
             ((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
d_unshifterTy_360 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                ((T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
C_T_52 T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v4))
      MAlonzo.Code.Raw.C__'183'__14 T_RawTy_2
v3 T_RawTy_2
v4
        -> (T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Raw.C__'183'__14
             ((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
d_unshifterTy_360 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
             ((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
d_unshifterTy_360 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v4))
      MAlonzo.Code.Raw.C_con_16 RTyCon
v3 -> T_RawTy_2 -> T_RawTy_2
forall a b. a -> b
coe T_RawTy_2
v2
      MAlonzo.Code.Raw.C_μ_18 T_RawTy_2
v3 T_RawTy_2
v4
        -> (T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Raw.C_μ_18
             ((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
d_unshifterTy_360 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
             ((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
d_unshifterTy_360 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v4))
      MAlonzo.Code.Raw.C_SOP_22 [[T_RawTy_2]]
v3
        -> ([[T_RawTy_2]] -> T_RawTy_2) -> Any -> T_RawTy_2
forall a b. a -> b
coe
             [[T_RawTy_2]] -> T_RawTy_2
MAlonzo.Code.Raw.C_SOP_22
             ((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]]
d_unshifterTyListList_372 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) ([[T_RawTy_2]] -> Any
forall a b. a -> b
coe [[T_RawTy_2]]
v3))
      T_RawTy_2
_ -> T_RawTy_2
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.unshifterTyList
d_unshifterTyList_366 ::
  Integer ->
  T_Weirdℕ_42 ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTy_2 ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTy_2
d_unshifterTyList_366 :: Integer -> T_Weirdℕ_42 -> [T_RawTy_2] -> [T_RawTy_2]
d_unshifterTyList_366 Integer
v0 T_Weirdℕ_42
v1 [T_RawTy_2]
v2
  = case [T_RawTy_2] -> [Any]
forall a b. a -> b
coe [T_RawTy_2]
v2 of
      [Any]
MAlonzo.Code.Utils.C_'91''93'_386 -> [T_RawTy_2] -> [T_RawTy_2]
forall a b. a -> b
coe [T_RawTy_2]
v2
      MAlonzo.Code.Utils.C__'8759'__388 Any
v3 [Any]
v4
        -> (Any -> [Any] -> [Any]) -> Any -> Any -> [T_RawTy_2]
forall a b. a -> b
coe
             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
             ((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
d_unshifterTy_360 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (Any -> Any
forall a b. a -> b
coe Any
v3))
             ((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]
d_unshifterTyList_366 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) ([Any] -> Any
forall a b. a -> b
coe [Any]
v4))
      [Any]
_ -> [T_RawTy_2]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.unshifterTyListList
d_unshifterTyListList_372 ::
  Integer ->
  T_Weirdℕ_42 ->
  MAlonzo.Code.Utils.T_List_382
    (MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTy_2) ->
  MAlonzo.Code.Utils.T_List_382
    (MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTy_2)
d_unshifterTyListList_372 :: Integer -> T_Weirdℕ_42 -> [[T_RawTy_2]] -> [[T_RawTy_2]]
d_unshifterTyListList_372 Integer
v0 T_Weirdℕ_42
v1 [[T_RawTy_2]]
v2
  = case [[T_RawTy_2]] -> [Any]
forall a b. a -> b
coe [[T_RawTy_2]]
v2 of
      [Any]
MAlonzo.Code.Utils.C_'91''93'_386 -> [[T_RawTy_2]] -> [[T_RawTy_2]]
forall a b. a -> b
coe [[T_RawTy_2]]
v2
      MAlonzo.Code.Utils.C__'8759'__388 Any
v3 [Any]
v4
        -> (Any -> [Any] -> [Any]) -> Any -> Any -> [[T_RawTy_2]]
forall a b. a -> b
coe
             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
             ((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]
d_unshifterTyList_366 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (Any -> Any
forall a b. a -> b
coe Any
v3))
             ((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]]
d_unshifterTyListList_372 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) ([Any] -> Any
forall a b. a -> b
coe [Any]
v4))
      [Any]
_ -> [[T_RawTy_2]]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.unshifter
d_unshifter_434 ::
  Integer ->
  T_Weirdℕ_42 ->
  MAlonzo.Code.Raw.T_RawTm_30 -> MAlonzo.Code.Raw.T_RawTm_30
d_unshifter_434 :: Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
d_unshifter_434 Integer
v0 T_Weirdℕ_42
v1 T_RawTm_30
v2
  = case T_RawTm_30 -> T_RawTm_30
forall a b. a -> b
coe T_RawTm_30
v2 of
      MAlonzo.Code.Raw.C_'96'_32 Integer
v3
        -> (Integer -> T_RawTm_30) -> Any -> T_RawTm_30
forall a b. a -> b
coe
             Integer -> T_RawTm_30
MAlonzo.Code.Raw.C_'96'_32
             ((Integer -> T_Weirdℕ_42 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> Integer
du_lookupWTm''_158 (Integer -> Any
forall a b. a -> b
coe Integer
v3) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1))
      MAlonzo.Code.Raw.C_Λ_34 KIND
v3 T_RawTm_30
v4
        -> (KIND -> T_RawTm_30 -> T_RawTm_30) -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             KIND -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Raw.C_Λ_34 (KIND -> Any
forall a b. a -> b
coe KIND
v3)
             ((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
d_unshifter_434 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                ((T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
C_T_52 T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v4))
      MAlonzo.Code.Raw.C__'183''8902'__36 T_RawTm_30
v3 T_RawTy_2
v4
        -> (T_RawTm_30 -> T_RawTy_2 -> T_RawTm_30) -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTm_30 -> T_RawTy_2 -> T_RawTm_30
MAlonzo.Code.Raw.C__'183''8902'__36
             ((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
d_unshifter_434 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v3))
             ((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
d_unshifterTy_360 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v4))
      MAlonzo.Code.Raw.C_ƛ_38 T_RawTy_2
v3 T_RawTm_30
v4
        -> (T_RawTy_2 -> T_RawTm_30 -> T_RawTm_30) -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Raw.C_ƛ_38
             ((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
d_unshifterTy_360 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ((T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
C_S_48 T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
             ((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
d_unshifter_434 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ((T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
C_S_48 T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v4))
      MAlonzo.Code.Raw.C__'183'__40 T_RawTm_30
v3 T_RawTm_30
v4
        -> (T_RawTm_30 -> T_RawTm_30 -> T_RawTm_30)
-> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTm_30 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Raw.C__'183'__40
             ((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
d_unshifter_434 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v3))
             ((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
d_unshifter_434 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v4))
      MAlonzo.Code.Raw.C_con_42 Some (ValueOf DefaultUni)
v3 -> T_RawTm_30 -> T_RawTm_30
forall a b. a -> b
coe T_RawTm_30
v2
      MAlonzo.Code.Raw.C_error_44 T_RawTy_2
v3
        -> (T_RawTy_2 -> T_RawTm_30) -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTm_30
MAlonzo.Code.Raw.C_error_44
             ((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
d_unshifterTy_360 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
      MAlonzo.Code.Raw.C_builtin_46 DefaultFun
v3 -> T_RawTm_30 -> T_RawTm_30
forall a b. a -> b
coe T_RawTm_30
v2
      MAlonzo.Code.Raw.C_wrap_48 T_RawTy_2
v3 T_RawTy_2
v4 T_RawTm_30
v5
        -> (T_RawTy_2 -> T_RawTy_2 -> T_RawTm_30 -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTy_2 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Raw.C_wrap_48
             ((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
d_unshifterTy_360 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
             ((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
d_unshifterTy_360 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v4))
             ((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
d_unshifter_434 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v5))
      MAlonzo.Code.Raw.C_unwrap_50 T_RawTm_30
v3
        -> (T_RawTm_30 -> T_RawTm_30) -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Raw.C_unwrap_50
             ((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
d_unshifter_434 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v3))
      MAlonzo.Code.Raw.C_constr_58 T_RawTy_2
v3 Integer
v4 [T_RawTm_30]
v5
        -> (T_RawTy_2 -> Integer -> [T_RawTm_30] -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTy_2 -> Integer -> [T_RawTm_30] -> T_RawTm_30
MAlonzo.Code.Raw.C_constr_58
             ((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
d_unshifterTy_360 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3)) (Integer -> Any
forall a b. a -> b
coe Integer
v4)
             ((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]
d_unshifterList_440 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) ([T_RawTm_30] -> Any
forall a b. a -> b
coe [T_RawTm_30]
v5))
      MAlonzo.Code.Raw.C_case_66 T_RawTy_2
v3 T_RawTm_30
v4 [T_RawTm_30]
v5
        -> (T_RawTy_2 -> T_RawTm_30 -> [T_RawTm_30] -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTm_30 -> [T_RawTm_30] -> T_RawTm_30
MAlonzo.Code.Raw.C_case_66
             ((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
d_unshifterTy_360 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
             ((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
d_unshifter_434 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v4))
             ((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]
d_unshifterList_440 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) ([T_RawTm_30] -> Any
forall a b. a -> b
coe [T_RawTm_30]
v5))
      T_RawTm_30
_ -> T_RawTm_30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.unshifterList
d_unshifterList_440 ::
  Integer ->
  T_Weirdℕ_42 ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTm_30 ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTm_30
d_unshifterList_440 :: Integer -> T_Weirdℕ_42 -> [T_RawTm_30] -> [T_RawTm_30]
d_unshifterList_440 Integer
v0 T_Weirdℕ_42
v1 [T_RawTm_30]
v2
  = case [T_RawTm_30] -> [Any]
forall a b. a -> b
coe [T_RawTm_30]
v2 of
      [Any]
MAlonzo.Code.Utils.C_'91''93'_386 -> [T_RawTm_30] -> [T_RawTm_30]
forall a b. a -> b
coe [T_RawTm_30]
v2
      MAlonzo.Code.Utils.C__'8759'__388 Any
v3 [Any]
v4
        -> (Any -> [Any] -> [Any]) -> Any -> Any -> [T_RawTm_30]
forall a b. a -> b
coe
             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
             ((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
d_unshifter_434 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (Any -> Any
forall a b. a -> b
coe Any
v3))
             ((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]
d_unshifterList_440 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) ([Any] -> Any
forall a b. a -> b
coe [Any]
v4))
      [Any]
_ -> [T_RawTm_30]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.ScopedTm
d_ScopedTm_522 :: p -> p -> ()
d_ScopedTm_522 p
a0 p
a1 = ()
data T_ScopedTm_522
  = C_'96'_528 T_WeirdFin_56 |
    C_Λ_530 MAlonzo.Code.Utils.T_Kind_476 T_ScopedTm_522 |
    C__'183''8902'__532 T_ScopedTm_522 T_ScopedTy_14 |
    C_ƛ_534 T_ScopedTy_14 T_ScopedTm_522 |
    C__'183'__536 T_ScopedTm_522 T_ScopedTm_522 |
    C_con_538 MAlonzo.Code.RawU.T_TmCon_198 |
    C_error_540 T_ScopedTy_14 |
    C_builtin_544 MAlonzo.Code.Builtin.T_Builtin_2 |
    C_wrap_546 T_ScopedTy_14 T_ScopedTy_14 T_ScopedTm_522 |
    C_unwrap_548 T_ScopedTm_522 |
    C_constr_556 T_ScopedTy_14 Integer
                 (MAlonzo.Code.Utils.T_List_382 T_ScopedTm_522) |
    C_case_564 T_ScopedTy_14 T_ScopedTm_522
               (MAlonzo.Code.Utils.T_List_382 T_ScopedTm_522)
-- Scoped.Tel
d_Tel_568 :: Integer -> T_Weirdℕ_42 -> Integer -> ()
d_Tel_568 :: Integer -> T_Weirdℕ_42 -> Integer -> ()
d_Tel_568 = Integer -> T_Weirdℕ_42 -> Integer -> ()
forall a. a
erased
-- Scoped.FreeVariableError
type T_FreeVariableError_574 = FreeVariableError
d_FreeVariableError_574 :: a
d_FreeVariableError_574
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Scoped.FreeVariableError"
-- Scoped.ScopeError
d_ScopeError_576 :: ()
d_ScopeError_576 = ()
type T_ScopeError_576 = ScopeError
pattern $mC_deBError_578 :: forall {r}. ScopeError -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_deBError_578 :: ScopeError
C_deBError_578 = DeBError
pattern $mC_freeVariableError_580 :: forall {r}.
ScopeError -> (FreeVariableError -> r) -> ((# #) -> r) -> r
$bC_freeVariableError_580 :: FreeVariableError -> ScopeError
C_freeVariableError_580 a0 = FreeVariableError a0
check_deBError_578 :: T_ScopeError_576
check_deBError_578 :: ScopeError
check_deBError_578 = ScopeError
DeBError
check_freeVariableError_580 ::
  T_FreeVariableError_574 -> T_ScopeError_576
check_freeVariableError_580 :: FreeVariableError -> ScopeError
check_freeVariableError_580 = FreeVariableError -> ScopeError
FreeVariableError
cover_ScopeError_576 :: ScopeError -> ()
cover_ScopeError_576 :: ScopeError -> ()
cover_ScopeError_576 ScopeError
x
  = case ScopeError
x of
      ScopeError
DeBError -> ()
      FreeVariableError FreeVariableError
_ -> ()
-- Scoped.ℕtoFin
d_ℕtoFin_584 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Utils.T_Either_6
    T_ScopeError_576 MAlonzo.Code.Data.Fin.Base.T_Fin_6
d_ℕtoFin_584 :: Integer -> Integer -> T_Either_6 ScopeError T_Fin_6
d_ℕtoFin_584 Integer
v0 Integer
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> (Any -> Either Any Any) -> Any -> T_Either_6 ScopeError T_Fin_6
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12 (ScopeError -> Any
forall a b. a -> b
coe ScopeError
C_deBError_578)
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T_Either_6 ScopeError T_Fin_6
forall a b. a -> b
coe
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
                Integer
0 -> (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe
                       Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                       (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
                Integer
_ -> let v3 :: Integer
v3 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                     Any -> Any
forall a b. a -> b
coe
                       ((T_Monad_186 -> (Any -> Any) -> Any -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                          T_Monad_186 -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Utils.du_fmap_224
                          (T_Monad_186 -> Any
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.du_EitherP_274)
                          ((T_Fin_6 -> T_Fin_6) -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16)
                          ((Integer -> Integer -> T_Either_6 ScopeError T_Fin_6)
-> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> T_Either_6 ScopeError T_Fin_6
d_ℕtoFin_584 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3))))
-- Scoped.ℕtoWeirdFin
d_ℕtoWeirdFin_596 ::
  Integer ->
  T_Weirdℕ_42 ->
  Integer ->
  MAlonzo.Code.Utils.T_Either_6 T_ScopeError_576 T_WeirdFin_56
d_ℕtoWeirdFin_596 :: Integer
-> T_Weirdℕ_42 -> Integer -> T_Either_6 ScopeError T_WeirdFin_56
d_ℕtoWeirdFin_596 ~Integer
v0 T_Weirdℕ_42
v1 Integer
v2 = T_Weirdℕ_42 -> Integer -> T_Either_6 ScopeError T_WeirdFin_56
du_ℕtoWeirdFin_596 T_Weirdℕ_42
v1 Integer
v2
du_ℕtoWeirdFin_596 ::
  T_Weirdℕ_42 ->
  Integer ->
  MAlonzo.Code.Utils.T_Either_6 T_ScopeError_576 T_WeirdFin_56
du_ℕtoWeirdFin_596 :: T_Weirdℕ_42 -> Integer -> T_Either_6 ScopeError T_WeirdFin_56
du_ℕtoWeirdFin_596 T_Weirdℕ_42
v0 Integer
v1
  = case T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
v0 of
      T_Weirdℕ_42
C_Z_44
        -> (Any -> Either Any Any)
-> Any -> T_Either_6 ScopeError T_WeirdFin_56
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12 (ScopeError -> Any
forall a b. a -> b
coe ScopeError
C_deBError_578)
      C_S_48 T_Weirdℕ_42
v3
        -> case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
             Integer
0 -> (Any -> Either Any Any)
-> Any -> T_Either_6 ScopeError T_WeirdFin_56
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 (T_WeirdFin_56 -> Any
forall a b. a -> b
coe T_WeirdFin_56
C_Z_62)
             Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                  Any -> T_Either_6 ScopeError T_WeirdFin_56
forall a b. a -> b
coe
                    ((Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                       Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                       ((T_Weirdℕ_42 -> Integer -> T_Either_6 ScopeError T_WeirdFin_56)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> Integer -> T_Either_6 ScopeError T_WeirdFin_56
du_ℕtoWeirdFin_596 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                       ((Any -> Any) -> Any
forall a b. a -> b
coe
                          (\ Any
v5 -> (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 ((T_WeirdFin_56 -> T_WeirdFin_56) -> Any -> Any
forall a b. a -> b
coe T_WeirdFin_56 -> T_WeirdFin_56
C_S_68 Any
v5))))
      C_T_52 T_Weirdℕ_42
v3
        -> (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> T_Either_6 ScopeError T_WeirdFin_56
forall a b. a -> b
coe
             Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             ((T_Weirdℕ_42 -> Integer -> T_Either_6 ScopeError T_WeirdFin_56)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> Integer -> T_Either_6 ScopeError T_WeirdFin_56
du_ℕtoWeirdFin_596 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v4 -> (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 ((T_WeirdFin_56 -> T_WeirdFin_56) -> Any -> Any
forall a b. a -> b
coe T_WeirdFin_56 -> T_WeirdFin_56
C_T_74 Any
v4)))
      T_Weirdℕ_42
_ -> T_Either_6 ScopeError T_WeirdFin_56
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.scopeCheckTy
d_scopeCheckTy_616 ::
  Integer ->
  MAlonzo.Code.Raw.T_RawTy_2 ->
  MAlonzo.Code.Utils.T_Either_6 T_ScopeError_576 T_ScopedTy_14
d_scopeCheckTy_616 :: Integer -> T_RawTy_2 -> T_Either_6 ScopeError T_ScopedTy_14
d_scopeCheckTy_616 Integer
v0 T_RawTy_2
v1
  = case T_RawTy_2 -> T_RawTy_2
forall a b. a -> b
coe T_RawTy_2
v1 of
      MAlonzo.Code.Raw.C_'96'_6 Integer
v2
        -> (T_Monad_186 -> (Any -> Any) -> Any -> Any)
-> Any -> Any -> Any -> T_Either_6 ScopeError T_ScopedTy_14
forall a b. a -> b
coe
             T_Monad_186 -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Utils.du_fmap_224
             (T_Monad_186 -> Any
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.du_EitherP_274) ((T_Fin_6 -> T_ScopedTy_14) -> Any
forall a b. a -> b
coe T_Fin_6 -> T_ScopedTy_14
C_'96'_18)
             ((Integer -> Integer -> T_Either_6 ScopeError T_Fin_6)
-> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> T_Either_6 ScopeError T_Fin_6
d_ℕtoFin_584 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
      MAlonzo.Code.Raw.C__'8658'__8 T_RawTy_2
v2 T_RawTy_2
v3
        -> (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> T_Either_6 ScopeError T_ScopedTy_14
forall a b. a -> b
coe
             Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             ((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
d_scopeCheckTy_616 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v2))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v4 ->
                   (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                     Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                     ((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
d_scopeCheckTy_616 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
                     ((Any -> Any) -> Any
forall a b. a -> b
coe
                        (\ Any
v5 ->
                           (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                             ((T_ScopedTy_14 -> T_ScopedTy_14 -> T_ScopedTy_14)
-> Any -> Any -> Any
forall a b. a -> b
coe T_ScopedTy_14 -> T_ScopedTy_14 -> T_ScopedTy_14
C__'8658'__20 (Any -> Any
forall a b. a -> b
coe Any
v4) (Any -> Any
forall a b. a -> b
coe Any
v5))))))
      MAlonzo.Code.Raw.C_Π_10 KIND
v2 T_RawTy_2
v3
        -> (T_Monad_186 -> (Any -> Any) -> Any -> Any)
-> Any -> Any -> Any -> T_Either_6 ScopeError T_ScopedTy_14
forall a b. a -> b
coe
             T_Monad_186 -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Utils.du_fmap_224
             (T_Monad_186 -> Any
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.du_EitherP_274) ((KIND -> T_ScopedTy_14 -> T_ScopedTy_14) -> Any -> Any
forall a b. a -> b
coe KIND -> T_ScopedTy_14 -> T_ScopedTy_14
C_Π_22 (KIND -> Any
forall a b. a -> b
coe KIND
v2))
             ((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
d_scopeCheckTy_616 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
      MAlonzo.Code.Raw.C_ƛ_12 KIND
v2 T_RawTy_2
v3
        -> (T_Monad_186 -> (Any -> Any) -> Any -> Any)
-> Any -> Any -> Any -> T_Either_6 ScopeError T_ScopedTy_14
forall a b. a -> b
coe
             T_Monad_186 -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Utils.du_fmap_224
             (T_Monad_186 -> Any
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.du_EitherP_274) ((KIND -> T_ScopedTy_14 -> T_ScopedTy_14) -> Any -> Any
forall a b. a -> b
coe KIND -> T_ScopedTy_14 -> T_ScopedTy_14
C_ƛ_24 (KIND -> Any
forall a b. a -> b
coe KIND
v2))
             ((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
d_scopeCheckTy_616 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
      MAlonzo.Code.Raw.C__'183'__14 T_RawTy_2
v2 T_RawTy_2
v3
        -> (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> T_Either_6 ScopeError T_ScopedTy_14
forall a b. a -> b
coe
             Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             ((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
d_scopeCheckTy_616 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v2))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v4 ->
                   (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                     Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                     ((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
d_scopeCheckTy_616 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
                     ((Any -> Any) -> Any
forall a b. a -> b
coe
                        (\ Any
v5 ->
                           (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                             ((T_ScopedTy_14 -> T_ScopedTy_14 -> T_ScopedTy_14)
-> Any -> Any -> Any
forall a b. a -> b
coe T_ScopedTy_14 -> T_ScopedTy_14 -> T_ScopedTy_14
C__'183'__26 (Any -> Any
forall a b. a -> b
coe Any
v4) (Any -> Any
forall a b. a -> b
coe Any
v5))))))
      MAlonzo.Code.Raw.C_con_16 RTyCon
v2
        -> case RTyCon -> RTyCon
forall a b. a -> b
coe RTyCon
v2 of
             MAlonzo.Code.Raw.C_atomic_24 AtomicTyCon
v3
               -> (Any -> Either Any Any)
-> Any -> T_Either_6 ScopeError T_ScopedTy_14
forall a b. a -> b
coe
                    Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                    ((KIND -> T_TyCon_6 -> T_ScopedTy_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                       KIND -> T_TyCon_6 -> T_ScopedTy_14
C_con_30 (KIND -> Any
forall a b. a -> b
coe KIND
MAlonzo.Code.Utils.C_'9839'_480)
                       ((AtomicTyCon -> T_TyCon_6) -> Any -> Any
forall a b. a -> b
coe AtomicTyCon -> T_TyCon_6
MAlonzo.Code.Builtin.Constant.Type.C_atomic_8 (AtomicTyCon -> Any
forall a b. a -> b
coe AtomicTyCon
v3)))
             RTyCon
MAlonzo.Code.Raw.C_list_26
               -> (Any -> Either Any Any)
-> Any -> T_Either_6 ScopeError T_ScopedTy_14
forall a b. a -> b
coe
                    Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                    ((KIND -> T_TyCon_6 -> T_ScopedTy_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                       KIND -> T_TyCon_6 -> T_ScopedTy_14
C_con_30
                       ((KIND -> KIND -> KIND) -> Any -> Any -> Any
forall a b. a -> b
coe
                          KIND -> KIND -> KIND
MAlonzo.Code.Utils.C__'8658'__482
                          (KIND -> Any
forall a b. a -> b
coe KIND
MAlonzo.Code.Utils.C_'9839'_480)
                          (KIND -> Any
forall a b. a -> b
coe KIND
MAlonzo.Code.Utils.C_'9839'_480))
                       (T_TyCon_6 -> Any
forall a b. a -> b
coe T_TyCon_6
MAlonzo.Code.Builtin.Constant.Type.C_list_10))
             RTyCon
MAlonzo.Code.Raw.C_pair_28
               -> (Any -> Either Any Any)
-> Any -> T_Either_6 ScopeError T_ScopedTy_14
forall a b. a -> b
coe
                    Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                    ((KIND -> T_TyCon_6 -> T_ScopedTy_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                       KIND -> T_TyCon_6 -> T_ScopedTy_14
C_con_30
                       ((KIND -> KIND -> KIND) -> Any -> Any -> Any
forall a b. a -> b
coe
                          KIND -> KIND -> KIND
MAlonzo.Code.Utils.C__'8658'__482
                          (KIND -> Any
forall a b. a -> b
coe KIND
MAlonzo.Code.Utils.C_'9839'_480)
                          ((KIND -> KIND -> KIND) -> Any -> Any -> Any
forall a b. a -> b
coe
                             KIND -> KIND -> KIND
MAlonzo.Code.Utils.C__'8658'__482
                             (KIND -> Any
forall a b. a -> b
coe KIND
MAlonzo.Code.Utils.C_'9839'_480)
                             (KIND -> Any
forall a b. a -> b
coe KIND
MAlonzo.Code.Utils.C_'9839'_480)))
                       (T_TyCon_6 -> Any
forall a b. a -> b
coe T_TyCon_6
MAlonzo.Code.Builtin.Constant.Type.C_pair_12))
             RTyCon
_ -> T_Either_6 ScopeError T_ScopedTy_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Raw.C_μ_18 T_RawTy_2
v2 T_RawTy_2
v3
        -> (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> T_Either_6 ScopeError T_ScopedTy_14
forall a b. a -> b
coe
             Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             ((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
d_scopeCheckTy_616 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v2))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v4 ->
                   (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                     Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                     ((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
d_scopeCheckTy_616 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
                     ((Any -> Any) -> Any
forall a b. a -> b
coe
                        (\ Any
v5 ->
                           (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                             ((T_ScopedTy_14 -> T_ScopedTy_14 -> T_ScopedTy_14)
-> Any -> Any -> Any
forall a b. a -> b
coe T_ScopedTy_14 -> T_ScopedTy_14 -> T_ScopedTy_14
C_μ_32 (Any -> Any
forall a b. a -> b
coe Any
v4) (Any -> Any
forall a b. a -> b
coe Any
v5))))))
      MAlonzo.Code.Raw.C_SOP_22 [[T_RawTy_2]]
v2
        -> (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> T_Either_6 ScopeError T_ScopedTy_14
forall a b. a -> b
coe
             Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             ((Integer
 -> [[T_RawTy_2]]
 -> T_Either_6 ScopeError (T_List_382 (T_List_382 T_ScopedTy_14)))
-> Any -> Any -> Any
forall a b. a -> b
coe Integer
-> [[T_RawTy_2]]
-> T_Either_6 ScopeError (T_List_382 (T_List_382 T_ScopedTy_14))
d_scopeCheckTyListList_624 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ([[T_RawTy_2]] -> Any
forall a b. a -> b
coe [[T_RawTy_2]]
v2))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v3 ->
                   (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 ((T_List_382 (T_List_382 T_ScopedTy_14) -> T_ScopedTy_14)
-> Any -> Any
forall a b. a -> b
coe T_List_382 (T_List_382 T_ScopedTy_14) -> T_ScopedTy_14
C_SOP_34 (Any -> Any
forall a b. a -> b
coe Any
v3))))
      T_RawTy_2
_ -> T_Either_6 ScopeError T_ScopedTy_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.scopeCheckTyList
d_scopeCheckTyList_620 ::
  Integer ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTy_2 ->
  MAlonzo.Code.Utils.T_Either_6
    T_ScopeError_576 (MAlonzo.Code.Utils.T_List_382 T_ScopedTy_14)
d_scopeCheckTyList_620 :: Integer
-> [T_RawTy_2] -> T_Either_6 ScopeError (T_List_382 T_ScopedTy_14)
d_scopeCheckTyList_620 Integer
v0 [T_RawTy_2]
v1
  = case [T_RawTy_2] -> [Any]
forall a b. a -> b
coe [T_RawTy_2]
v1 of
      [Any]
MAlonzo.Code.Utils.C_'91''93'_386
        -> (Any -> Either Any Any)
-> Any -> T_Either_6 ScopeError (T_List_382 T_ScopedTy_14)
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 ([T_RawTy_2] -> Any
forall a b. a -> b
coe [T_RawTy_2]
v1)
      MAlonzo.Code.Utils.C__'8759'__388 Any
v2 [Any]
v3
        -> (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> T_Either_6 ScopeError (T_List_382 T_ScopedTy_14)
forall a b. a -> b
coe
             Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             ((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
d_scopeCheckTy_616 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Any -> Any
forall a b. a -> b
coe Any
v2))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v4 ->
                   (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                     Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                     ((Integer
 -> [T_RawTy_2] -> T_Either_6 ScopeError (T_List_382 T_ScopedTy_14))
-> Any -> Any -> Any
forall a b. a -> b
coe Integer
-> [T_RawTy_2] -> T_Either_6 ScopeError (T_List_382 T_ScopedTy_14)
d_scopeCheckTyList_620 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ([Any] -> Any
forall a b. a -> b
coe [Any]
v3))
                     ((Any -> Any) -> Any
forall a b. a -> b
coe
                        (\ Any
v5 ->
                           (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                             ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388 (Any -> Any
forall a b. a -> b
coe Any
v4) (Any -> Any
forall a b. a -> b
coe Any
v5))))))
      [Any]
_ -> T_Either_6 ScopeError (T_List_382 T_ScopedTy_14)
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.scopeCheckTyListList
d_scopeCheckTyListList_624 ::
  Integer ->
  MAlonzo.Code.Utils.T_List_382
    (MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTy_2) ->
  MAlonzo.Code.Utils.T_Either_6
    T_ScopeError_576
    (MAlonzo.Code.Utils.T_List_382
       (MAlonzo.Code.Utils.T_List_382 T_ScopedTy_14))
d_scopeCheckTyListList_624 :: Integer
-> [[T_RawTy_2]]
-> T_Either_6 ScopeError (T_List_382 (T_List_382 T_ScopedTy_14))
d_scopeCheckTyListList_624 Integer
v0 [[T_RawTy_2]]
v1
  = case [[T_RawTy_2]] -> [Any]
forall a b. a -> b
coe [[T_RawTy_2]]
v1 of
      [Any]
MAlonzo.Code.Utils.C_'91''93'_386
        -> (Any -> Either Any Any)
-> Any
-> T_Either_6 ScopeError (T_List_382 (T_List_382 T_ScopedTy_14))
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 ([[T_RawTy_2]] -> Any
forall a b. a -> b
coe [[T_RawTy_2]]
v1)
      MAlonzo.Code.Utils.C__'8759'__388 Any
v2 [Any]
v3
        -> (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any
-> Any
-> T_Either_6 ScopeError (T_List_382 (T_List_382 T_ScopedTy_14))
forall a b. a -> b
coe
             Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             ((Integer
 -> [T_RawTy_2] -> T_Either_6 ScopeError (T_List_382 T_ScopedTy_14))
-> Any -> Any -> Any
forall a b. a -> b
coe Integer
-> [T_RawTy_2] -> T_Either_6 ScopeError (T_List_382 T_ScopedTy_14)
d_scopeCheckTyList_620 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Any -> Any
forall a b. a -> b
coe Any
v2))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v4 ->
                   (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                     Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                     ((Integer
 -> [[T_RawTy_2]]
 -> T_Either_6 ScopeError (T_List_382 (T_List_382 T_ScopedTy_14)))
-> Any -> Any -> Any
forall a b. a -> b
coe Integer
-> [[T_RawTy_2]]
-> T_Either_6 ScopeError (T_List_382 (T_List_382 T_ScopedTy_14))
d_scopeCheckTyListList_624 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ([Any] -> Any
forall a b. a -> b
coe [Any]
v3))
                     ((Any -> Any) -> Any
forall a b. a -> b
coe
                        (\ Any
v5 ->
                           (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                             ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388 (Any -> Any
forall a b. a -> b
coe Any
v4) (Any -> Any
forall a b. a -> b
coe Any
v5))))))
      [Any]
_ -> T_Either_6 ScopeError (T_List_382 (T_List_382 T_ScopedTy_14))
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.scopeCheckTm
d_scopeCheckTm_686 ::
  Integer ->
  T_Weirdℕ_42 ->
  MAlonzo.Code.Raw.T_RawTm_30 ->
  MAlonzo.Code.Utils.T_Either_6 T_ScopeError_576 T_ScopedTm_522
d_scopeCheckTm_686 :: Integer
-> T_Weirdℕ_42
-> T_RawTm_30
-> T_Either_6 ScopeError T_ScopedTm_522
d_scopeCheckTm_686 Integer
v0 T_Weirdℕ_42
v1 T_RawTm_30
v2
  = case T_RawTm_30 -> T_RawTm_30
forall a b. a -> b
coe T_RawTm_30
v2 of
      MAlonzo.Code.Raw.C_'96'_32 Integer
v3
        -> (T_Monad_186 -> (Any -> Any) -> Any -> Any)
-> Any -> Any -> Any -> T_Either_6 ScopeError T_ScopedTm_522
forall a b. a -> b
coe
             T_Monad_186 -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Utils.du_fmap_224
             (T_Monad_186 -> Any
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.du_EitherP_274) ((T_WeirdFin_56 -> T_ScopedTm_522) -> Any
forall a b. a -> b
coe T_WeirdFin_56 -> T_ScopedTm_522
C_'96'_528)
             ((T_Weirdℕ_42 -> Integer -> T_Either_6 ScopeError T_WeirdFin_56)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> Integer -> T_Either_6 ScopeError T_WeirdFin_56
du_ℕtoWeirdFin_596 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v3))
      MAlonzo.Code.Raw.C_Λ_34 KIND
v3 T_RawTm_30
v4
        -> (T_Monad_186 -> (Any -> Any) -> Any -> Any)
-> Any -> Any -> Any -> T_Either_6 ScopeError T_ScopedTm_522
forall a b. a -> b
coe
             T_Monad_186 -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Utils.du_fmap_224
             (T_Monad_186 -> Any
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.du_EitherP_274) ((KIND -> T_ScopedTm_522 -> T_ScopedTm_522) -> Any -> Any
forall a b. a -> b
coe KIND -> T_ScopedTm_522 -> T_ScopedTm_522
C_Λ_530 (KIND -> Any
forall a b. a -> b
coe KIND
v3))
             ((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
d_scopeCheckTm_686 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                ((T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
C_T_52 T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v4))
      MAlonzo.Code.Raw.C__'183''8902'__36 T_RawTm_30
v3 T_RawTy_2
v4
        -> (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> T_Either_6 ScopeError T_ScopedTm_522
forall a b. a -> b
coe
             Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             ((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
d_scopeCheckTy_616 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v4))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v5 ->
                   (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                     Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                     ((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
d_scopeCheckTm_686 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v3))
                     ((Any -> Any) -> Any
forall a b. a -> b
coe
                        (\ Any
v6 ->
                           (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                             ((T_ScopedTm_522 -> T_ScopedTy_14 -> T_ScopedTm_522)
-> Any -> Any -> Any
forall a b. a -> b
coe T_ScopedTm_522 -> T_ScopedTy_14 -> T_ScopedTm_522
C__'183''8902'__532 (Any -> Any
forall a b. a -> b
coe Any
v6) (Any -> Any
forall a b. a -> b
coe Any
v5))))))
      MAlonzo.Code.Raw.C_ƛ_38 T_RawTy_2
v3 T_RawTm_30
v4
        -> (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> T_Either_6 ScopeError T_ScopedTm_522
forall a b. a -> b
coe
             Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             ((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
d_scopeCheckTy_616 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v5 ->
                   (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                     Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                     ((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
d_scopeCheckTm_686 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ((T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
C_S_48 T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v4))
                     ((Any -> Any) -> Any
forall a b. a -> b
coe
                        (\ Any
v6 ->
                           (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                             ((T_ScopedTy_14 -> T_ScopedTm_522 -> T_ScopedTm_522)
-> Any -> Any -> Any
forall a b. a -> b
coe T_ScopedTy_14 -> T_ScopedTm_522 -> T_ScopedTm_522
C_ƛ_534 (Any -> Any
forall a b. a -> b
coe Any
v5) (Any -> Any
forall a b. a -> b
coe Any
v6))))))
      MAlonzo.Code.Raw.C__'183'__40 T_RawTm_30
v3 T_RawTm_30
v4
        -> (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> T_Either_6 ScopeError T_ScopedTm_522
forall a b. a -> b
coe
             Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             ((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
d_scopeCheckTm_686 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v3))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v5 ->
                   (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                     Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                     ((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
d_scopeCheckTm_686 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v4))
                     ((Any -> Any) -> Any
forall a b. a -> b
coe
                        (\ Any
v6 ->
                           (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                             ((T_ScopedTm_522 -> T_ScopedTm_522 -> T_ScopedTm_522)
-> Any -> Any -> Any
forall a b. a -> b
coe T_ScopedTm_522 -> T_ScopedTm_522 -> T_ScopedTm_522
C__'183'__536 (Any -> Any
forall a b. a -> b
coe Any
v5) (Any -> Any
forall a b. a -> b
coe Any
v6))))))
      MAlonzo.Code.Raw.C_con_42 Some (ValueOf DefaultUni)
v3
        -> (Any -> Either Any Any)
-> Any -> T_Either_6 ScopeError T_ScopedTm_522
forall a b. a -> b
coe
             Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
             ((T_TmCon_198 -> T_ScopedTm_522) -> Any -> Any
forall a b. a -> b
coe T_TmCon_198 -> T_ScopedTm_522
C_con_538 ((Some (ValueOf DefaultUni) -> T_TmCon_198) -> Any -> Any
forall a b. a -> b
coe Some (ValueOf DefaultUni) -> T_TmCon_198
MAlonzo.Code.RawU.d_tagCon2TmCon_226 (Some (ValueOf DefaultUni) -> Any
forall a b. a -> b
coe Some (ValueOf DefaultUni)
v3)))
      MAlonzo.Code.Raw.C_error_44 T_RawTy_2
v3
        -> (T_Monad_186 -> (Any -> Any) -> Any -> Any)
-> Any -> Any -> Any -> T_Either_6 ScopeError T_ScopedTm_522
forall a b. a -> b
coe
             T_Monad_186 -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Utils.du_fmap_224
             (T_Monad_186 -> Any
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.du_EitherP_274) ((T_ScopedTy_14 -> T_ScopedTm_522) -> Any
forall a b. a -> b
coe T_ScopedTy_14 -> T_ScopedTm_522
C_error_540)
             ((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
d_scopeCheckTy_616 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
      MAlonzo.Code.Raw.C_builtin_46 DefaultFun
v3
        -> (Any -> Either Any Any)
-> Any -> T_Either_6 ScopeError T_ScopedTm_522
forall a b. a -> b
coe
             Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 ((DefaultFun -> T_ScopedTm_522) -> Any -> Any
forall a b. a -> b
coe DefaultFun -> T_ScopedTm_522
C_builtin_544 (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
v3))
      MAlonzo.Code.Raw.C_wrap_48 T_RawTy_2
v3 T_RawTy_2
v4 T_RawTm_30
v5
        -> (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> T_Either_6 ScopeError T_ScopedTm_522
forall a b. a -> b
coe
             Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             ((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
d_scopeCheckTy_616 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v6 ->
                   (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                     Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                     ((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
d_scopeCheckTy_616 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v4))
                     ((Any -> Any) -> Any
forall a b. a -> b
coe
                        (\ Any
v7 ->
                           (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                             Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                             ((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
d_scopeCheckTm_686 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v5))
                             ((Any -> Any) -> Any
forall a b. a -> b
coe
                                (\ Any
v8 ->
                                   (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe
                                     Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                                     ((T_ScopedTy_14
 -> T_ScopedTy_14 -> T_ScopedTm_522 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_ScopedTy_14 -> T_ScopedTy_14 -> T_ScopedTm_522 -> T_ScopedTm_522
C_wrap_546 (Any -> Any
forall a b. a -> b
coe Any
v6) (Any -> Any
forall a b. a -> b
coe Any
v7) (Any -> Any
forall a b. a -> b
coe Any
v8))))))))
      MAlonzo.Code.Raw.C_unwrap_50 T_RawTm_30
v3
        -> (T_Monad_186 -> (Any -> Any) -> Any -> Any)
-> Any -> Any -> Any -> T_Either_6 ScopeError T_ScopedTm_522
forall a b. a -> b
coe
             T_Monad_186 -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Utils.du_fmap_224
             (T_Monad_186 -> Any
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.du_EitherP_274) ((T_ScopedTm_522 -> T_ScopedTm_522) -> Any
forall a b. a -> b
coe T_ScopedTm_522 -> T_ScopedTm_522
C_unwrap_548)
             ((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
d_scopeCheckTm_686 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v3))
      MAlonzo.Code.Raw.C_constr_58 T_RawTy_2
v3 Integer
v4 [T_RawTm_30]
v5
        -> (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> T_Either_6 ScopeError T_ScopedTm_522
forall a b. a -> b
coe
             Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             ((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
d_scopeCheckTy_616 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v6 ->
                   (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                     Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                     ((Integer
 -> T_Weirdℕ_42
 -> [T_RawTm_30]
 -> T_Either_6 ScopeError (T_List_382 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_List_382 T_ScopedTm_522)
d_scopeCheckTmList_692 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) ([T_RawTm_30] -> Any
forall a b. a -> b
coe [T_RawTm_30]
v5))
                     ((Any -> Any) -> Any
forall a b. a -> b
coe
                        (\ Any
v7 ->
                           (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                             ((T_ScopedTy_14
 -> Integer -> T_List_382 T_ScopedTm_522 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_ScopedTy_14
-> Integer -> T_List_382 T_ScopedTm_522 -> T_ScopedTm_522
C_constr_556 (Any -> Any
forall a b. a -> b
coe Any
v6) (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Any -> Any
forall a b. a -> b
coe Any
v7))))))
      MAlonzo.Code.Raw.C_case_66 T_RawTy_2
v3 T_RawTm_30
v4 [T_RawTm_30]
v5
        -> (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> T_Either_6 ScopeError T_ScopedTm_522
forall a b. a -> b
coe
             Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             ((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
d_scopeCheckTy_616 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_RawTy_2 -> Any
forall a b. a -> b
coe T_RawTy_2
v3))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v6 ->
                   (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                     Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                     ((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
d_scopeCheckTm_686 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_RawTm_30 -> Any
forall a b. a -> b
coe T_RawTm_30
v4))
                     ((Any -> Any) -> Any
forall a b. a -> b
coe
                        (\ Any
v7 ->
                           (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                             Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                             ((Integer
 -> T_Weirdℕ_42
 -> [T_RawTm_30]
 -> T_Either_6 ScopeError (T_List_382 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_List_382 T_ScopedTm_522)
d_scopeCheckTmList_692 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) ([T_RawTm_30] -> Any
forall a b. a -> b
coe [T_RawTm_30]
v5))
                             ((Any -> Any) -> Any
forall a b. a -> b
coe
                                (\ Any
v8 ->
                                   (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe
                                     Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                                     ((T_ScopedTy_14
 -> T_ScopedTm_522 -> T_List_382 T_ScopedTm_522 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_ScopedTy_14
-> T_ScopedTm_522 -> T_List_382 T_ScopedTm_522 -> T_ScopedTm_522
C_case_564 (Any -> Any
forall a b. a -> b
coe Any
v6) (Any -> Any
forall a b. a -> b
coe Any
v7) (Any -> Any
forall a b. a -> b
coe Any
v8))))))))
      T_RawTm_30
_ -> T_Either_6 ScopeError T_ScopedTm_522
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.scopeCheckTmList
d_scopeCheckTmList_692 ::
  Integer ->
  T_Weirdℕ_42 ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTm_30 ->
  MAlonzo.Code.Utils.T_Either_6
    T_ScopeError_576 (MAlonzo.Code.Utils.T_List_382 T_ScopedTm_522)
d_scopeCheckTmList_692 :: Integer
-> T_Weirdℕ_42
-> [T_RawTm_30]
-> T_Either_6 ScopeError (T_List_382 T_ScopedTm_522)
d_scopeCheckTmList_692 Integer
v0 T_Weirdℕ_42
v1 [T_RawTm_30]
v2
  = case [T_RawTm_30] -> [Any]
forall a b. a -> b
coe [T_RawTm_30]
v2 of
      [Any]
MAlonzo.Code.Utils.C_'91''93'_386
        -> (Any -> Either Any Any)
-> Any -> T_Either_6 ScopeError (T_List_382 T_ScopedTm_522)
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 ([T_RawTm_30] -> Any
forall a b. a -> b
coe [T_RawTm_30]
v2)
      MAlonzo.Code.Utils.C__'8759'__388 Any
v3 [Any]
v4
        -> (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> T_Either_6 ScopeError (T_List_382 T_ScopedTm_522)
forall a b. a -> b
coe
             Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             ((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
d_scopeCheckTm_686 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (Any -> Any
forall a b. a -> b
coe Any
v3))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v5 ->
                   (Either Any Any -> (Any -> Either Any Any) -> Either Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                     Either Any Any -> (Any -> Either Any Any) -> Either Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                     ((Integer
 -> T_Weirdℕ_42
 -> [T_RawTm_30]
 -> T_Either_6 ScopeError (T_List_382 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_List_382 T_ScopedTm_522)
d_scopeCheckTmList_692 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) ([Any] -> Any
forall a b. a -> b
coe [Any]
v4))
                     ((Any -> Any) -> Any
forall a b. a -> b
coe
                        (\ Any
v6 ->
                           (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                             ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388 (Any -> Any
forall a b. a -> b
coe Any
v5) (Any -> Any
forall a b. a -> b
coe Any
v6))))))
      [Any]
_ -> T_Either_6 ScopeError (T_List_382 T_ScopedTm_522)
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.extricateScopeTy
d_extricateScopeTy_780 ::
  Integer -> T_ScopedTy_14 -> MAlonzo.Code.Raw.T_RawTy_2
d_extricateScopeTy_780 :: Integer -> T_ScopedTy_14 -> T_RawTy_2
d_extricateScopeTy_780 Integer
v0 T_ScopedTy_14
v1
  = case T_ScopedTy_14 -> T_ScopedTy_14
forall a b. a -> b
coe T_ScopedTy_14
v1 of
      C_'96'_18 T_Fin_6
v2
        -> (Integer -> T_RawTy_2) -> Any -> T_RawTy_2
forall a b. a -> b
coe
             Integer -> T_RawTy_2
MAlonzo.Code.Raw.C_'96'_6
             ((T_Fin_6 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> Integer
MAlonzo.Code.Data.Fin.Base.du_toℕ_20 (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v2))
      C__'8658'__20 T_ScopedTy_14
v2 T_ScopedTy_14
v3
        -> (T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Raw.C__'8658'__8
             ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_ScopedTy_14 -> T_RawTy_2
d_extricateScopeTy_780 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_ScopedTy_14 -> Any
forall a b. a -> b
coe T_ScopedTy_14
v2))
             ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_ScopedTy_14 -> T_RawTy_2
d_extricateScopeTy_780 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_ScopedTy_14 -> Any
forall a b. a -> b
coe T_ScopedTy_14
v3))
      C_Π_22 KIND
v2 T_ScopedTy_14
v3
        -> (KIND -> T_RawTy_2 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
             KIND -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Raw.C_Π_10 (KIND -> Any
forall a b. a -> b
coe KIND
v2)
             ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> Any
forall a b. a -> b
coe
                Integer -> T_ScopedTy_14 -> T_RawTy_2
d_extricateScopeTy_780 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                (T_ScopedTy_14 -> Any
forall a b. a -> b
coe T_ScopedTy_14
v3))
      C_ƛ_24 KIND
v2 T_ScopedTy_14
v3
        -> (KIND -> T_RawTy_2 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
             KIND -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Raw.C_ƛ_12 (KIND -> Any
forall a b. a -> b
coe KIND
v2)
             ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> Any
forall a b. a -> b
coe
                Integer -> T_ScopedTy_14 -> T_RawTy_2
d_extricateScopeTy_780 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                (T_ScopedTy_14 -> Any
forall a b. a -> b
coe T_ScopedTy_14
v3))
      C__'183'__26 T_ScopedTy_14
v2 T_ScopedTy_14
v3
        -> (T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Raw.C__'183'__14
             ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_ScopedTy_14 -> T_RawTy_2
d_extricateScopeTy_780 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_ScopedTy_14 -> Any
forall a b. a -> b
coe T_ScopedTy_14
v2))
             ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_ScopedTy_14 -> T_RawTy_2
d_extricateScopeTy_780 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_ScopedTy_14 -> Any
forall a b. a -> b
coe T_ScopedTy_14
v3))
      C_con_30 KIND
v2 T_TyCon_6
v3
        -> case T_TyCon_6 -> T_TyCon_6
forall a b. a -> b
coe T_TyCon_6
v3 of
             MAlonzo.Code.Builtin.Constant.Type.C_atomic_8 AtomicTyCon
v4
               -> (RTyCon -> T_RawTy_2) -> Any -> T_RawTy_2
forall a b. a -> b
coe
                    RTyCon -> T_RawTy_2
MAlonzo.Code.Raw.C_con_16
                    ((AtomicTyCon -> RTyCon) -> Any -> Any
forall a b. a -> b
coe AtomicTyCon -> RTyCon
MAlonzo.Code.Raw.C_atomic_24 (AtomicTyCon -> Any
forall a b. a -> b
coe AtomicTyCon
v4))
             T_TyCon_6
MAlonzo.Code.Builtin.Constant.Type.C_list_10
               -> (RTyCon -> T_RawTy_2) -> Any -> T_RawTy_2
forall a b. a -> b
coe RTyCon -> T_RawTy_2
MAlonzo.Code.Raw.C_con_16 (RTyCon -> Any
forall a b. a -> b
coe RTyCon
MAlonzo.Code.Raw.C_list_26)
             T_TyCon_6
MAlonzo.Code.Builtin.Constant.Type.C_pair_12
               -> (RTyCon -> T_RawTy_2) -> Any -> T_RawTy_2
forall a b. a -> b
coe RTyCon -> T_RawTy_2
MAlonzo.Code.Raw.C_con_16 (RTyCon -> Any
forall a b. a -> b
coe RTyCon
MAlonzo.Code.Raw.C_pair_28)
             T_TyCon_6
_ -> T_RawTy_2
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_μ_32 T_ScopedTy_14
v2 T_ScopedTy_14
v3
        -> (T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Raw.C_μ_18
             ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_ScopedTy_14 -> T_RawTy_2
d_extricateScopeTy_780 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_ScopedTy_14 -> Any
forall a b. a -> b
coe T_ScopedTy_14
v2))
             ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_ScopedTy_14 -> T_RawTy_2
d_extricateScopeTy_780 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_ScopedTy_14 -> Any
forall a b. a -> b
coe T_ScopedTy_14
v3))
      C_SOP_34 T_List_382 (T_List_382 T_ScopedTy_14)
v2
        -> ([[T_RawTy_2]] -> T_RawTy_2) -> Any -> T_RawTy_2
forall a b. a -> b
coe
             [[T_RawTy_2]] -> T_RawTy_2
MAlonzo.Code.Raw.C_SOP_22
             ((Integer -> T_List_382 (T_List_382 T_ScopedTy_14) -> [[T_RawTy_2]])
-> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_List_382 (T_List_382 T_ScopedTy_14) -> [[T_RawTy_2]]
d_extricateScopeTyListList_788 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_List_382 (T_List_382 T_ScopedTy_14) -> Any
forall a b. a -> b
coe T_List_382 (T_List_382 T_ScopedTy_14)
v2))
      T_ScopedTy_14
_ -> T_RawTy_2
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.extricateScopeTyList
d_extricateScopeTyList_784 ::
  Integer ->
  MAlonzo.Code.Utils.T_List_382 T_ScopedTy_14 ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTy_2
d_extricateScopeTyList_784 :: Integer -> T_List_382 T_ScopedTy_14 -> [T_RawTy_2]
d_extricateScopeTyList_784 Integer
v0 T_List_382 T_ScopedTy_14
v1
  = case T_List_382 T_ScopedTy_14 -> [Any]
forall a b. a -> b
coe T_List_382 T_ScopedTy_14
v1 of
      [Any]
MAlonzo.Code.Utils.C_'91''93'_386 -> T_List_382 T_ScopedTy_14 -> [T_RawTy_2]
forall a b. a -> b
coe T_List_382 T_ScopedTy_14
v1
      MAlonzo.Code.Utils.C__'8759'__388 Any
v2 [Any]
v3
        -> (Any -> [Any] -> [Any]) -> Any -> Any -> [T_RawTy_2]
forall a b. a -> b
coe
             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
             ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_ScopedTy_14 -> T_RawTy_2
d_extricateScopeTy_780 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Any -> Any
forall a b. a -> b
coe Any
v2))
             ((Integer -> T_List_382 T_ScopedTy_14 -> [T_RawTy_2])
-> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_List_382 T_ScopedTy_14 -> [T_RawTy_2]
d_extricateScopeTyList_784 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ([Any] -> Any
forall a b. a -> b
coe [Any]
v3))
      [Any]
_ -> [T_RawTy_2]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.extricateScopeTyListList
d_extricateScopeTyListList_788 ::
  Integer ->
  MAlonzo.Code.Utils.T_List_382
    (MAlonzo.Code.Utils.T_List_382 T_ScopedTy_14) ->
  MAlonzo.Code.Utils.T_List_382
    (MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTy_2)
d_extricateScopeTyListList_788 :: Integer -> T_List_382 (T_List_382 T_ScopedTy_14) -> [[T_RawTy_2]]
d_extricateScopeTyListList_788 Integer
v0 T_List_382 (T_List_382 T_ScopedTy_14)
v1
  = case T_List_382 (T_List_382 T_ScopedTy_14) -> [Any]
forall a b. a -> b
coe T_List_382 (T_List_382 T_ScopedTy_14)
v1 of
      [Any]
MAlonzo.Code.Utils.C_'91''93'_386 -> T_List_382 (T_List_382 T_ScopedTy_14) -> [[T_RawTy_2]]
forall a b. a -> b
coe T_List_382 (T_List_382 T_ScopedTy_14)
v1
      MAlonzo.Code.Utils.C__'8759'__388 Any
v2 [Any]
v3
        -> (Any -> [Any] -> [Any]) -> Any -> Any -> [[T_RawTy_2]]
forall a b. a -> b
coe
             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
             ((Integer -> T_List_382 T_ScopedTy_14 -> [T_RawTy_2])
-> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_List_382 T_ScopedTy_14 -> [T_RawTy_2]
d_extricateScopeTyList_784 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Any -> Any
forall a b. a -> b
coe Any
v2))
             ((Integer -> T_List_382 (T_List_382 T_ScopedTy_14) -> [[T_RawTy_2]])
-> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_List_382 (T_List_382 T_ScopedTy_14) -> [[T_RawTy_2]]
d_extricateScopeTyListList_788 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ([Any] -> Any
forall a b. a -> b
coe [Any]
v3))
      [Any]
_ -> [[T_RawTy_2]]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.extricateScope
d_extricateScope_828 ::
  Integer ->
  T_Weirdℕ_42 -> T_ScopedTm_522 -> MAlonzo.Code.Raw.T_RawTm_30
d_extricateScope_828 :: Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
d_extricateScope_828 Integer
v0 T_Weirdℕ_42
v1 T_ScopedTm_522
v2
  = case T_ScopedTm_522 -> T_ScopedTm_522
forall a b. a -> b
coe T_ScopedTm_522
v2 of
      C_'96'_528 T_WeirdFin_56
v3
        -> (Integer -> T_RawTm_30) -> Any -> T_RawTm_30
forall a b. a -> b
coe
             Integer -> T_RawTm_30
MAlonzo.Code.Raw.C_'96'_32
             ((T_Weirdℕ_42 -> T_WeirdFin_56 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_WeirdFin_56 -> Integer
du_WeirdFintoℕ_88 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_WeirdFin_56 -> Any
forall a b. a -> b
coe T_WeirdFin_56
v3))
      C_Λ_530 KIND
v3 T_ScopedTm_522
v4
        -> (KIND -> T_RawTm_30 -> T_RawTm_30) -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             KIND -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Raw.C_Λ_34 (KIND -> Any
forall a b. a -> b
coe KIND
v3)
             ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
d_extricateScope_828 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
                ((T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
C_T_52 T_Weirdℕ_42
v1) (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v4))
      C__'183''8902'__532 T_ScopedTm_522
v3 T_ScopedTy_14
v4
        -> (T_RawTm_30 -> T_RawTy_2 -> T_RawTm_30) -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTm_30 -> T_RawTy_2 -> T_RawTm_30
MAlonzo.Code.Raw.C__'183''8902'__36
             ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
d_extricateScope_828 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v3))
             ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_ScopedTy_14 -> T_RawTy_2
d_extricateScopeTy_780 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_ScopedTy_14 -> Any
forall a b. a -> b
coe T_ScopedTy_14
v4))
      C_ƛ_534 T_ScopedTy_14
v3 T_ScopedTm_522
v4
        -> (T_RawTy_2 -> T_RawTm_30 -> T_RawTm_30) -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Raw.C_ƛ_38
             ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_ScopedTy_14 -> T_RawTy_2
d_extricateScopeTy_780 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_ScopedTy_14 -> Any
forall a b. a -> b
coe T_ScopedTy_14
v3))
             ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
d_extricateScope_828 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ((T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
C_S_48 T_Weirdℕ_42
v1) (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v4))
      C__'183'__536 T_ScopedTm_522
v3 T_ScopedTm_522
v4
        -> (T_RawTm_30 -> T_RawTm_30 -> T_RawTm_30)
-> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTm_30 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Raw.C__'183'__40
             ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
d_extricateScope_828 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v3))
             ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
d_extricateScope_828 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v4))
      C_con_538 T_TmCon_198
v3
        -> (Some (ValueOf DefaultUni) -> T_RawTm_30) -> Any -> T_RawTm_30
forall a b. a -> b
coe
             Some (ValueOf DefaultUni) -> T_RawTm_30
MAlonzo.Code.Raw.C_con_42
             ((T_TmCon_198 -> Some (ValueOf DefaultUni)) -> Any -> Any
forall a b. a -> b
coe T_TmCon_198 -> Some (ValueOf DefaultUni)
MAlonzo.Code.RawU.d_tmCon2TagCon_316 (T_TmCon_198 -> Any
forall a b. a -> b
coe T_TmCon_198
v3))
      C_error_540 T_ScopedTy_14
v3
        -> (T_RawTy_2 -> T_RawTm_30) -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTm_30
MAlonzo.Code.Raw.C_error_44
             ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_ScopedTy_14 -> T_RawTy_2
d_extricateScopeTy_780 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_ScopedTy_14 -> Any
forall a b. a -> b
coe T_ScopedTy_14
v3))
      C_builtin_544 DefaultFun
v3 -> (DefaultFun -> T_RawTm_30) -> Any -> T_RawTm_30
forall a b. a -> b
coe DefaultFun -> T_RawTm_30
MAlonzo.Code.Raw.C_builtin_46 (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
v3)
      C_wrap_546 T_ScopedTy_14
v3 T_ScopedTy_14
v4 T_ScopedTm_522
v5
        -> (T_RawTy_2 -> T_RawTy_2 -> T_RawTm_30 -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTy_2 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Raw.C_wrap_48
             ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_ScopedTy_14 -> T_RawTy_2
d_extricateScopeTy_780 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_ScopedTy_14 -> Any
forall a b. a -> b
coe T_ScopedTy_14
v3))
             ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_ScopedTy_14 -> T_RawTy_2
d_extricateScopeTy_780 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_ScopedTy_14 -> Any
forall a b. a -> b
coe T_ScopedTy_14
v4))
             ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
d_extricateScope_828 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v5))
      C_unwrap_548 T_ScopedTm_522
v3
        -> (T_RawTm_30 -> T_RawTm_30) -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Raw.C_unwrap_50
             ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
d_extricateScope_828 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v3))
      C_constr_556 T_ScopedTy_14
v3 Integer
v4 T_List_382 T_ScopedTm_522
v5
        -> (T_RawTy_2 -> Integer -> [T_RawTm_30] -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTy_2 -> Integer -> [T_RawTm_30] -> T_RawTm_30
MAlonzo.Code.Raw.C_constr_58
             ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_ScopedTy_14 -> T_RawTy_2
d_extricateScopeTy_780 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_ScopedTy_14 -> Any
forall a b. a -> b
coe T_ScopedTy_14
v3)) (Integer -> Any
forall a b. a -> b
coe Integer
v4)
             ((Integer
 -> T_Weirdℕ_42 -> T_List_382 T_ScopedTm_522 -> [T_RawTm_30])
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> T_List_382 T_ScopedTm_522 -> [T_RawTm_30]
d_extricateScopeList_834 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_List_382 T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_List_382 T_ScopedTm_522
v5))
      C_case_564 T_ScopedTy_14
v3 T_ScopedTm_522
v4 T_List_382 T_ScopedTm_522
v5
        -> (T_RawTy_2 -> T_RawTm_30 -> [T_RawTm_30] -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
             T_RawTy_2 -> T_RawTm_30 -> [T_RawTm_30] -> T_RawTm_30
MAlonzo.Code.Raw.C_case_66
             ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_ScopedTy_14 -> T_RawTy_2
d_extricateScopeTy_780 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_ScopedTy_14 -> Any
forall a b. a -> b
coe T_ScopedTy_14
v3))
             ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
d_extricateScope_828 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v4))
             ((Integer
 -> T_Weirdℕ_42 -> T_List_382 T_ScopedTm_522 -> [T_RawTm_30])
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> T_List_382 T_ScopedTm_522 -> [T_RawTm_30]
d_extricateScopeList_834 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (T_List_382 T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_List_382 T_ScopedTm_522
v5))
      T_ScopedTm_522
_ -> T_RawTm_30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.extricateScopeList
d_extricateScopeList_834 ::
  Integer ->
  T_Weirdℕ_42 ->
  MAlonzo.Code.Utils.T_List_382 T_ScopedTm_522 ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Raw.T_RawTm_30
d_extricateScopeList_834 :: Integer -> T_Weirdℕ_42 -> T_List_382 T_ScopedTm_522 -> [T_RawTm_30]
d_extricateScopeList_834 Integer
v0 T_Weirdℕ_42
v1 T_List_382 T_ScopedTm_522
v2
  = case T_List_382 T_ScopedTm_522 -> [Any]
forall a b. a -> b
coe T_List_382 T_ScopedTm_522
v2 of
      [Any]
MAlonzo.Code.Utils.C_'91''93'_386 -> T_List_382 T_ScopedTm_522 -> [T_RawTm_30]
forall a b. a -> b
coe T_List_382 T_ScopedTm_522
v2
      MAlonzo.Code.Utils.C__'8759'__388 Any
v3 [Any]
v4
        -> (Any -> [Any] -> [Any]) -> Any -> Any -> [T_RawTm_30]
forall a b. a -> b
coe
             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
             ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
d_extricateScope_828 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) (Any -> Any
forall a b. a -> b
coe Any
v3))
             ((Integer
 -> T_Weirdℕ_42 -> T_List_382 T_ScopedTm_522 -> [T_RawTm_30])
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Weirdℕ_42 -> T_List_382 T_ScopedTm_522 -> [T_RawTm_30]
d_extricateScopeList_834 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v1) ([Any] -> Any
forall a b. a -> b
coe [Any]
v4))
      [Any]
_ -> [T_RawTm_30]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.uglyWeirdFin
d_uglyWeirdFin_888 ::
  Integer ->
  T_Weirdℕ_42 ->
  T_WeirdFin_56 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_uglyWeirdFin_888 :: Integer -> T_Weirdℕ_42 -> T_WeirdFin_56 -> Text
d_uglyWeirdFin_888 ~Integer
v0 T_Weirdℕ_42
v1 T_WeirdFin_56
v2 = T_Weirdℕ_42 -> T_WeirdFin_56 -> Text
du_uglyWeirdFin_888 T_Weirdℕ_42
v1 T_WeirdFin_56
v2
du_uglyWeirdFin_888 ::
  T_Weirdℕ_42 ->
  T_WeirdFin_56 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
du_uglyWeirdFin_888 :: T_Weirdℕ_42 -> T_WeirdFin_56 -> Text
du_uglyWeirdFin_888 T_Weirdℕ_42
v0 T_WeirdFin_56
v1
  = case T_WeirdFin_56 -> T_WeirdFin_56
forall a b. a -> b
coe T_WeirdFin_56
v1 of
      T_WeirdFin_56
C_Z_62 -> Text -> Text
forall a b. a -> b
coe (Text
"0" :: Data.Text.Text)
      C_S_68 T_WeirdFin_56
v4
        -> case T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
v0 of
             C_S_48 T_Weirdℕ_42
v6
               -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
                    Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                    (Text
"(S " :: Data.Text.Text)
                    ((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
                       Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                       ((T_Weirdℕ_42 -> T_WeirdFin_56 -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_WeirdFin_56 -> Text
du_uglyWeirdFin_888 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v6) (T_WeirdFin_56 -> Any
forall a b. a -> b
coe T_WeirdFin_56
v4))
                       (Text
")" :: Data.Text.Text))
             T_Weirdℕ_42
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_T_74 T_WeirdFin_56
v4
        -> case T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
v0 of
             C_T_52 T_Weirdℕ_42
v6
               -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
                    Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                    (Text
"(T " :: Data.Text.Text)
                    ((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
                       Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                       ((T_Weirdℕ_42 -> T_WeirdFin_56 -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_WeirdFin_56 -> Text
du_uglyWeirdFin_888 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v6) (T_WeirdFin_56 -> Any
forall a b. a -> b
coe T_WeirdFin_56
v4))
                       (Text
")" :: Data.Text.Text))
             T_Weirdℕ_42
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_WeirdFin_56
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.uglyTmCon
d_uglyTmCon_894 ::
  MAlonzo.Code.RawU.T_TmCon_198 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_uglyTmCon_894 :: T_TmCon_198 -> Text
d_uglyTmCon_894 T_TmCon_198
v0
  = case T_TmCon_198 -> T_TmCon_198
forall a b. a -> b
coe T_TmCon_198
v0 of
      MAlonzo.Code.RawU.C_tmCon_202 T__'8866''9839'_4
v1 Any
v2
        -> let v3 :: Text
v3 = Text
"size" :: Data.Text.Text in
           Any -> Text
forall a b. a -> b
coe
             (case T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe T__'8866''9839'_4
v1 of
                MAlonzo.Code.Builtin.Signature.C_atomic_12 AtomicTyCon
v5
                  -> case AtomicTyCon -> AtomicTyCon
forall a b. a -> b
coe AtomicTyCon
v5 of
                       AtomicTyCon
MAlonzo.Code.Builtin.Constant.AtomicType.C_aInteger_8
                         -> (Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                              (Text
"(integer " :: Data.Text.Text)
                              ((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
                                 Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                 (Integer -> Text
MAlonzo.Code.Data.Integer.Show.d_show_6 (Any -> Integer
forall a b. a -> b
coe Any
v2))
                                 (Text
")" :: Data.Text.Text))
                       AtomicTyCon
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBytestring_10
                         -> Text -> Any
forall a b. a -> b
coe (Text
"bytestring" :: Data.Text.Text)
                       AtomicTyCon
_ -> Text -> Any
forall a b. a -> b
coe Text
v3
                T__'8866''9839'_4
_ -> Text -> Any
forall a b. a -> b
coe Text
v3)
      T_TmCon_198
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.showNat
d_showNat_902 ::
  Integer -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showNat_902 :: Integer -> Text
d_showNat_902 = [Char] -> Text
T.pack ([Char] -> Text) -> (Integer -> [Char]) -> Integer -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> [Char]
forall a. Show a => a -> [Char]
show
-- Scoped.uglyBuiltin
d_uglyBuiltin_904 ::
  MAlonzo.Code.Builtin.T_Builtin_2 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_uglyBuiltin_904 :: DefaultFun -> Text
d_uglyBuiltin_904 DefaultFun
v0
  = let v1 :: Text
v1 = Text
"other" :: Data.Text.Text in
    Any -> Text
forall a b. a -> b
coe
      (case DefaultFun -> DefaultFun
forall a b. a -> b
coe DefaultFun
v0 of
         DefaultFun
MAlonzo.Code.Builtin.C_addInteger_4
           -> Text -> Any
forall a b. a -> b
coe (Text
"addInteger" :: Data.Text.Text)
         DefaultFun
_ -> Text -> Any
forall a b. a -> b
coe Text
v1)
-- Scoped.ugly
d_ugly_910 ::
  Integer ->
  T_Weirdℕ_42 ->
  T_ScopedTm_522 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_ugly_910 :: Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> Text
d_ugly_910 ~Integer
v0 T_Weirdℕ_42
v1 T_ScopedTm_522
v2 = T_Weirdℕ_42 -> T_ScopedTm_522 -> Text
du_ugly_910 T_Weirdℕ_42
v1 T_ScopedTm_522
v2
du_ugly_910 ::
  T_Weirdℕ_42 ->
  T_ScopedTm_522 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
du_ugly_910 :: T_Weirdℕ_42 -> T_ScopedTm_522 -> Text
du_ugly_910 T_Weirdℕ_42
v0 T_ScopedTm_522
v1
  = case T_ScopedTm_522 -> T_ScopedTm_522
forall a b. a -> b
coe T_ScopedTm_522
v1 of
      C_'96'_528 T_WeirdFin_56
v2
        -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"(` " :: Data.Text.Text)
             ((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                ((T_Weirdℕ_42 -> T_WeirdFin_56 -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_WeirdFin_56 -> Text
du_uglyWeirdFin_888 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v0) (T_WeirdFin_56 -> Any
forall a b. a -> b
coe T_WeirdFin_56
v2))
                (Text
")" :: Data.Text.Text))
      C_Λ_530 KIND
v2 T_ScopedTm_522
v3
        -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"(\923 " :: Data.Text.Text)
             ((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                ((T_Weirdℕ_42 -> T_ScopedTm_522 -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_ScopedTm_522 -> Text
du_ugly_910 ((T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
C_T_52 T_Weirdℕ_42
v0) (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v3)) (Text
")" :: Data.Text.Text))
      C__'183''8902'__532 T_ScopedTm_522
v2 T_ScopedTy_14
v3
        -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"( " :: Data.Text.Text)
             ((Text -> Text -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                ((T_Weirdℕ_42 -> T_ScopedTm_522 -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_ScopedTm_522 -> Text
du_ugly_910 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v0) (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v2))
                ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                   Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                   (Text
" \183\8902 " :: Data.Text.Text)
                   ((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
"TYPE" :: Data.Text.Text) (Text
")" :: Data.Text.Text))))
      C_ƛ_534 T_ScopedTy_14
v2 T_ScopedTm_522
v3
        -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"(\411 " :: Data.Text.Text)
             ((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                ((T_Weirdℕ_42 -> T_ScopedTm_522 -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_ScopedTm_522 -> Text
du_ugly_910 ((T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
C_S_48 T_Weirdℕ_42
v0) (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v3)) (Text
")" :: Data.Text.Text))
      C__'183'__536 T_ScopedTm_522
v2 T_ScopedTm_522
v3
        -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"( " :: Data.Text.Text)
             ((Text -> Text -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                ((T_Weirdℕ_42 -> T_ScopedTm_522 -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_ScopedTm_522 -> Text
du_ugly_910 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v0) (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v2))
                ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                   Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                   (Text
" \183 " :: Data.Text.Text)
                   ((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
                      Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                      ((T_Weirdℕ_42 -> T_ScopedTm_522 -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_ScopedTm_522 -> Text
du_ugly_910 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v0) (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v3)) (Text
")" :: Data.Text.Text))))
      C_con_538 T_TmCon_198
v2 -> Text -> Text
forall a b. a -> b
coe (Text
"(con " :: Data.Text.Text)
      C_error_540 T_ScopedTy_14
v2 -> Text -> Text
forall a b. a -> b
coe (Text
"error _" :: Data.Text.Text)
      C_builtin_544 DefaultFun
v2
        -> (Text -> Text -> Text) -> Text -> Text -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"builtin " :: Data.Text.Text) (DefaultFun -> Text
d_uglyBuiltin_904 (DefaultFun -> DefaultFun
forall a b. a -> b
coe DefaultFun
v2))
      C_wrap_546 T_ScopedTy_14
v2 T_ScopedTy_14
v3 T_ScopedTm_522
v4
        -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"(wrap " :: Data.Text.Text)
             ((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                ((T_Weirdℕ_42 -> T_ScopedTm_522 -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_ScopedTm_522 -> Text
du_ugly_910 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v0) (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v4)) (Text
")" :: Data.Text.Text))
      C_unwrap_548 T_ScopedTm_522
v2
        -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"(unwrap " :: Data.Text.Text)
             ((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                ((T_Weirdℕ_42 -> T_ScopedTm_522 -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe T_Weirdℕ_42 -> T_ScopedTm_522 -> Text
du_ugly_910 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
v0) (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v2)) (Text
")" :: Data.Text.Text))
      C_constr_556 T_ScopedTy_14
v2 Integer
v3 T_List_382 T_ScopedTm_522
v4 -> Text -> Text
forall a b. a -> b
coe (Text
"constr" :: Data.Text.Text)
      C_case_564 T_ScopedTy_14
v2 T_ScopedTm_522
v3 T_List_382 T_ScopedTm_522
v4 -> Text -> Text
forall a b. a -> b
coe (Text
"case" :: Data.Text.Text)
      T_ScopedTm_522
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError