{-# 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.Extrication 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.Algorithmic
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.Data.Vec.Base
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Scoped
import qualified MAlonzo.Code.Type
import qualified MAlonzo.Code.Type.BetaNBE
import qualified MAlonzo.Code.Type.BetaNormal
import qualified MAlonzo.Code.Utils
import qualified MAlonzo.Code.Utils.List

-- Scoped.Extrication.len⋆
d_len'8902'_4 :: MAlonzo.Code.Type.T_Ctx'8902'_2 -> Integer
d_len'8902'_4 :: T_Ctx'8902'_2 -> Integer
d_len'8902'_4 T_Ctx'8902'_2
v0
  = case T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0 of
      T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      MAlonzo.Code.Type.C__'44''8902'__6 T_Ctx'8902'_2
v1 T_Kind_476
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_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2 -> Integer
d_len'8902'_4 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v1))
      T_Ctx'8902'_2
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.Extrication.extricateVar⋆
d_extricateVar'8902'_16 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_10
d_extricateVar'8902'_16 :: T_Ctx'8902'_2 -> T_Kind_476 -> T__'8715''8902'__14 -> T_Fin_10
d_extricateVar'8902'_16 T_Ctx'8902'_2
v0 ~T_Kind_476
v1 T__'8715''8902'__14
v2 = T_Ctx'8902'_2 -> T__'8715''8902'__14 -> T_Fin_10
du_extricateVar'8902'_16 T_Ctx'8902'_2
v0 T__'8715''8902'__14
v2
du_extricateVar'8902'_16 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 ->
  MAlonzo.Code.Data.Fin.Base.T_Fin_10
du_extricateVar'8902'_16 :: T_Ctx'8902'_2 -> T__'8715''8902'__14 -> T_Fin_10
du_extricateVar'8902'_16 T_Ctx'8902'_2
v0 T__'8715''8902'__14
v1
  = case T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T__'8715''8902'__14
v1 of
      T__'8715''8902'__14
MAlonzo.Code.Type.C_Z_16
        -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
      MAlonzo.Code.Type.C_S_18 T__'8715''8902'__14
v5
        -> case T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0 of
             MAlonzo.Code.Type.C__'44''8902'__6 T_Ctx'8902'_2
v6 T_Kind_476
v7
               -> (T_Fin_10 -> T_Fin_10) -> Any -> T_Fin_10
forall a b. a -> b
coe
                    T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                    ((T_Ctx'8902'_2 -> T__'8715''8902'__14 -> T_Fin_10)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2 -> T__'8715''8902'__14 -> T_Fin_10
du_extricateVar'8902'_16 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v6) (T__'8715''8902'__14 -> Any
forall a b. a -> b
coe T__'8715''8902'__14
v5))
             T_Ctx'8902'_2
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8715''8902'__14
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.Extrication.extricateNf⋆
d_extricateNf'8902'_26 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Scoped.T_ScopedTy_14
d_extricateNf'8902'_26 :: T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
d_extricateNf'8902'_26 T_Ctx'8902'_2
v0 T_Kind_476
v1 T__'8866'Nf'8902'__4
v2
  = case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2 of
      MAlonzo.Code.Type.BetaNormal.C_Π_14 T_Kind_476
v4 T__'8866'Nf'8902'__4
v5
        -> (T_Kind_476 -> T_ScopedTy_14 -> T_ScopedTy_14)
-> Any -> Any -> T_ScopedTy_14
forall a b. a -> b
coe
             T_Kind_476 -> T_ScopedTy_14 -> T_ScopedTy_14
MAlonzo.Code.Scoped.C_Π_22 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v4)
             ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
d_extricateNf'8902'_26
                ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2) -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v4))
                (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478) (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v5))
      MAlonzo.Code.Type.BetaNormal.C__'8658'__16 T__'8866'Nf'8902'__4
v4 T__'8866'Nf'8902'__4
v5
        -> (T_ScopedTy_14 -> T_ScopedTy_14 -> T_ScopedTy_14)
-> Any -> Any -> T_ScopedTy_14
forall a b. a -> b
coe
             T_ScopedTy_14 -> T_ScopedTy_14 -> T_ScopedTy_14
MAlonzo.Code.Scoped.C__'8658'__20
             ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
d_extricateNf'8902'_26 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)
                (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v4))
             ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
d_extricateNf'8902'_26 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)
                (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v5))
      MAlonzo.Code.Type.BetaNormal.C_ƛ_18 T__'8866'Nf'8902'__4
v6
        -> case T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v1 of
             MAlonzo.Code.Utils.C__'8658'__482 T_Kind_476
v7 T_Kind_476
v8
               -> (T_Kind_476 -> T_ScopedTy_14 -> T_ScopedTy_14)
-> Any -> Any -> T_ScopedTy_14
forall a b. a -> b
coe
                    T_Kind_476 -> T_ScopedTy_14 -> T_ScopedTy_14
MAlonzo.Code.Scoped.C_ƛ_24 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v7)
                    ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
d_extricateNf'8902'_26
                       ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2) -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v7)) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v8)
                       (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v6))
             T_Kind_476
_ -> T_ScopedTy_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Type.BetaNormal.C_ne_20 T__'8866'Ne'8902'__6
v5
        -> (T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Ne'8902'__6 -> T_ScopedTy_14)
-> Any -> Any -> Any -> T_ScopedTy_14
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Ne'8902'__6 -> T_ScopedTy_14
d_extricateNe'8902'_34 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v1) (T__'8866'Ne'8902'__6 -> Any
forall a b. a -> b
coe T__'8866'Ne'8902'__6
v5)
      MAlonzo.Code.Type.BetaNormal.C_con_22 T__'8866'Nf'8902'__4
v4
        -> case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v4 of
             MAlonzo.Code.Type.BetaNormal.C_ne_20 T__'8866'Ne'8902'__6
v7
               -> (T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Ne'8902'__6 -> T_ScopedTy_14)
-> Any -> Any -> Any -> T_ScopedTy_14
forall a b. a -> b
coe
                    T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Ne'8902'__6 -> T_ScopedTy_14
d_extricateNe'8902'_34 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                    (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'9839'_480) (T__'8866'Ne'8902'__6 -> Any
forall a b. a -> b
coe T__'8866'Ne'8902'__6
v7)
             T__'8866'Nf'8902'__4
_ -> T_ScopedTy_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Type.BetaNormal.C_μ_24 T_Kind_476
v4 T__'8866'Nf'8902'__4
v5 T__'8866'Nf'8902'__4
v6
        -> (T_ScopedTy_14 -> T_ScopedTy_14 -> T_ScopedTy_14)
-> Any -> Any -> T_ScopedTy_14
forall a b. a -> b
coe
             T_ScopedTy_14 -> T_ScopedTy_14 -> T_ScopedTy_14
MAlonzo.Code.Scoped.C_μ_32
             ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
d_extricateNf'8902'_26 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                   T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482
                   ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v4)
                      (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                   ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                      T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v4)
                      (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
                (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v5))
             ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
d_extricateNf'8902'_26 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v4) (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v6))
      MAlonzo.Code.Type.BetaNormal.C_SOP_28 Integer
v4 T_Vec_28
v5
        -> (T_List_382 (T_List_382 T_ScopedTy_14) -> T_ScopedTy_14)
-> Any -> T_ScopedTy_14
forall a b. a -> b
coe
             T_List_382 (T_List_382 T_ScopedTy_14) -> T_ScopedTy_14
MAlonzo.Code.Scoped.C_SOP_34
             ((T_Ctx'8902'_2
 -> T_Kind_476 -> T_Vec_28 -> T_List_382 (T_List_382 T_ScopedTy_14))
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Kind_476 -> T_Vec_28 -> T_List_382 (T_List_382 T_ScopedTy_14)
du_extricateNf'8902''45'VecList_56 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478) (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v5))
      T__'8866'Nf'8902'__4
_ -> T_ScopedTy_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.Extrication.extricateNe⋆
d_extricateNe'8902'_34 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Ne'8902'__6 ->
  MAlonzo.Code.Scoped.T_ScopedTy_14
d_extricateNe'8902'_34 :: T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Ne'8902'__6 -> T_ScopedTy_14
d_extricateNe'8902'_34 T_Ctx'8902'_2
v0 T_Kind_476
v1 T__'8866'Ne'8902'__6
v2
  = case T__'8866'Ne'8902'__6 -> T__'8866'Ne'8902'__6
forall a b. a -> b
coe T__'8866'Ne'8902'__6
v2 of
      MAlonzo.Code.Type.BetaNormal.C_'96'_8 T__'8715''8902'__14
v5
        -> (T_Fin_10 -> T_ScopedTy_14) -> Any -> T_ScopedTy_14
forall a b. a -> b
coe
             T_Fin_10 -> T_ScopedTy_14
MAlonzo.Code.Scoped.C_'96'_18
             ((T_Ctx'8902'_2 -> T__'8715''8902'__14 -> T_Fin_10)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2 -> T__'8715''8902'__14 -> T_Fin_10
du_extricateVar'8902'_16 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T__'8715''8902'__14 -> Any
forall a b. a -> b
coe T__'8715''8902'__14
v5))
      MAlonzo.Code.Type.BetaNormal.C__'183'__10 T_Kind_476
v4 T__'8866'Ne'8902'__6
v6 T__'8866'Nf'8902'__4
v7
        -> (T_ScopedTy_14 -> T_ScopedTy_14 -> T_ScopedTy_14)
-> Any -> Any -> T_ScopedTy_14
forall a b. a -> b
coe
             T_ScopedTy_14 -> T_ScopedTy_14 -> T_ScopedTy_14
MAlonzo.Code.Scoped.C__'183'__26
             ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Ne'8902'__6 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Ne'8902'__6 -> T_ScopedTy_14
d_extricateNe'8902'_34 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v4) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v1)) (T__'8866'Ne'8902'__6 -> Any
forall a b. a -> b
coe T__'8866'Ne'8902'__6
v6))
             ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
d_extricateNf'8902'_26 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v4) (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v7))
      MAlonzo.Code.Type.BetaNormal.C_'94'_12 T_TyCon_6
v5
        -> (T_Kind_476 -> T_TyCon_6 -> T_ScopedTy_14)
-> Any -> Any -> T_ScopedTy_14
forall a b. a -> b
coe T_Kind_476 -> T_TyCon_6 -> T_ScopedTy_14
MAlonzo.Code.Scoped.C_con_30 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v1) (T_TyCon_6 -> Any
forall a b. a -> b
coe T_TyCon_6
v5)
      T__'8866'Ne'8902'__6
_ -> T_ScopedTy_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.Extrication.extricateNf⋆-List
d_extricateNf'8902''45'List_42 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Scoped.T_ScopedTy_14
d_extricateNf'8902''45'List_42 :: T_Ctx'8902'_2
-> T_Kind_476 -> [T__'8866'Nf'8902'__4] -> T_List_382 T_ScopedTy_14
d_extricateNf'8902''45'List_42 T_Ctx'8902'_2
v0 T_Kind_476
v1 [T__'8866'Nf'8902'__4]
v2
  = case [T__'8866'Nf'8902'__4] -> [Any]
forall a b. a -> b
coe [T__'8866'Nf'8902'__4]
v2 of
      [] -> [Any] -> T_List_382 T_ScopedTy_14
forall a b. a -> b
coe [Any]
forall {a}. [a]
MAlonzo.Code.Utils.C_'91''93'_386
      (:) Any
v3 [Any]
v4
        -> (Any -> [Any] -> [Any]) -> Any -> Any -> T_List_382 T_ScopedTy_14
forall a b. a -> b
coe
             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
             ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
d_extricateNf'8902'_26 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v1) (Any -> Any
forall a b. a -> b
coe Any
v3))
             ((T_Ctx'8902'_2
 -> T_Kind_476
 -> [T__'8866'Nf'8902'__4]
 -> T_List_382 T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Kind_476 -> [T__'8866'Nf'8902'__4] -> T_List_382 T_ScopedTy_14
d_extricateNf'8902''45'List_42 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v1) ([Any] -> Any
forall a b. a -> b
coe [Any]
v4))
      [Any]
_ -> T_List_382 T_ScopedTy_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.Extrication.extricateNf⋆-VecList
d_extricateNf'8902''45'VecList_56 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  Integer ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Utils.T_List_382
    (MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Scoped.T_ScopedTy_14)
d_extricateNf'8902''45'VecList_56 :: T_Ctx'8902'_2
-> T_Kind_476
-> Integer
-> T_Vec_28
-> T_List_382 (T_List_382 T_ScopedTy_14)
d_extricateNf'8902''45'VecList_56 T_Ctx'8902'_2
v0 T_Kind_476
v1 ~Integer
v2 T_Vec_28
v3
  = T_Ctx'8902'_2
-> T_Kind_476 -> T_Vec_28 -> T_List_382 (T_List_382 T_ScopedTy_14)
du_extricateNf'8902''45'VecList_56 T_Ctx'8902'_2
v0 T_Kind_476
v1 T_Vec_28
v3
du_extricateNf'8902''45'VecList_56 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Utils.T_List_382
    (MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Scoped.T_ScopedTy_14)
du_extricateNf'8902''45'VecList_56 :: T_Ctx'8902'_2
-> T_Kind_476 -> T_Vec_28 -> T_List_382 (T_List_382 T_ScopedTy_14)
du_extricateNf'8902''45'VecList_56 T_Ctx'8902'_2
v0 T_Kind_476
v1 T_Vec_28
v2
  = case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v2 of
      T_Vec_28
MAlonzo.Code.Data.Vec.Base.C_'91''93'_32
        -> [Any] -> T_List_382 (T_List_382 T_ScopedTy_14)
forall a b. a -> b
coe [Any]
forall {a}. [a]
MAlonzo.Code.Utils.C_'91''93'_386
      MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v4 T_Vec_28
v5
        -> (Any -> [Any] -> [Any])
-> Any -> Any -> T_List_382 (T_List_382 T_ScopedTy_14)
forall a b. a -> b
coe
             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
             ((T_Ctx'8902'_2
 -> T_Kind_476
 -> [T__'8866'Nf'8902'__4]
 -> T_List_382 T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Kind_476 -> [T__'8866'Nf'8902'__4] -> T_List_382 T_ScopedTy_14
d_extricateNf'8902''45'List_42 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v1) (Any -> Any
forall a b. a -> b
coe Any
v4))
             ((T_Ctx'8902'_2
 -> T_Kind_476 -> T_Vec_28 -> T_List_382 (T_List_382 T_ScopedTy_14))
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Kind_476 -> T_Vec_28 -> T_List_382 (T_List_382 T_ScopedTy_14)
du_extricateNf'8902''45'VecList_56 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v1) (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v5))
      T_Vec_28
_ -> T_List_382 (T_List_382 T_ScopedTy_14)
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.Extrication.len
d_len_94 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Algorithmic.T_Ctx_2 -> MAlonzo.Code.Scoped.T_Weirdℕ_42
d_len_94 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T_Weirdℕ_42
d_len_94 T_Ctx'8902'_2
v0 T_Ctx_2
v1
  = case T_Ctx_2 -> T_Ctx_2
forall a b. a -> b
coe T_Ctx_2
v1 of
      T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4
        -> T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44
      MAlonzo.Code.Algorithmic.C__'44''8902'__8 T_Ctx_2
v3
        -> case T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0 of
             MAlonzo.Code.Type.C__'44''8902'__6 T_Ctx'8902'_2
v5 T_Kind_476
v6
               -> (T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
MAlonzo.Code.Scoped.C_T_52 (T_Ctx'8902'_2 -> T_Ctx_2 -> T_Weirdℕ_42
d_len_94 (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v5) (T_Ctx_2 -> T_Ctx_2
forall a b. a -> b
coe T_Ctx_2
v3))
             T_Ctx'8902'_2
_ -> T_Weirdℕ_42
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Algorithmic.C__'44'__12 T_Ctx_2
v3 T__'8866'Nf'8902'__4
v4
        -> (T_Weirdℕ_42 -> T_Weirdℕ_42) -> T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42 -> T_Weirdℕ_42
MAlonzo.Code.Scoped.C_S_48 (T_Ctx'8902'_2 -> T_Ctx_2 -> T_Weirdℕ_42
d_len_94 (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> T_Ctx_2
forall a b. a -> b
coe T_Ctx_2
v3))
      T_Ctx_2
_ -> T_Weirdℕ_42
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.Extrication.extricateVar
d_extricateVar_110 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Algorithmic.T_Ctx_2 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Algorithmic.T__'8715'__16 ->
  MAlonzo.Code.Scoped.T_WeirdFin_56
d_extricateVar_110 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8715'__16
-> T_WeirdFin_56
d_extricateVar_110 T_Ctx'8902'_2
v0 T_Ctx_2
v1 ~T__'8866'Nf'8902'__4
v2 T__'8715'__16
v3 = T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8715'__16 -> T_WeirdFin_56
du_extricateVar_110 T_Ctx'8902'_2
v0 T_Ctx_2
v1 T__'8715'__16
v3
du_extricateVar_110 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Algorithmic.T_Ctx_2 ->
  MAlonzo.Code.Algorithmic.T__'8715'__16 ->
  MAlonzo.Code.Scoped.T_WeirdFin_56
du_extricateVar_110 :: T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8715'__16 -> T_WeirdFin_56
du_extricateVar_110 T_Ctx'8902'_2
v0 T_Ctx_2
v1 T__'8715'__16
v2
  = case T__'8715'__16 -> T__'8715'__16
forall a b. a -> b
coe T__'8715'__16
v2 of
      T__'8715'__16
MAlonzo.Code.Algorithmic.C_Z_22 -> T_WeirdFin_56 -> T_WeirdFin_56
forall a b. a -> b
coe T_WeirdFin_56
MAlonzo.Code.Scoped.C_Z_62
      MAlonzo.Code.Algorithmic.C_S_30 T__'8715'__16
v7
        -> case T_Ctx_2 -> T_Ctx_2
forall a b. a -> b
coe T_Ctx_2
v1 of
             MAlonzo.Code.Algorithmic.C__'44'__12 T_Ctx_2
v9 T__'8866'Nf'8902'__4
v10
               -> (T_WeirdFin_56 -> T_WeirdFin_56) -> Any -> T_WeirdFin_56
forall a b. a -> b
coe
                    T_WeirdFin_56 -> T_WeirdFin_56
MAlonzo.Code.Scoped.C_S_68
                    ((T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8715'__16 -> T_WeirdFin_56)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8715'__16 -> T_WeirdFin_56
du_extricateVar_110 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
v9) (T__'8715'__16 -> Any
forall a b. a -> b
coe T__'8715'__16
v7))
             T_Ctx_2
_ -> T_WeirdFin_56
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Algorithmic.C_T_38 T__'8866'Nf'8902'__4
v6 T__'8715'__16
v7
        -> case T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0 of
             MAlonzo.Code.Type.C__'44''8902'__6 T_Ctx'8902'_2
v8 T_Kind_476
v9
               -> case T_Ctx_2 -> T_Ctx_2
forall a b. a -> b
coe T_Ctx_2
v1 of
                    MAlonzo.Code.Algorithmic.C__'44''8902'__8 T_Ctx_2
v11
                      -> (T_WeirdFin_56 -> T_WeirdFin_56) -> Any -> T_WeirdFin_56
forall a b. a -> b
coe
                           T_WeirdFin_56 -> T_WeirdFin_56
MAlonzo.Code.Scoped.C_T_74
                           ((T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8715'__16 -> T_WeirdFin_56)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8715'__16 -> T_WeirdFin_56
du_extricateVar_110 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v8) (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
v11) (T__'8715'__16 -> Any
forall a b. a -> b
coe T__'8715'__16
v7))
                    T_Ctx_2
_ -> T_WeirdFin_56
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Ctx'8902'_2
_ -> T_WeirdFin_56
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8715'__16
_ -> T_WeirdFin_56
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.Extrication.extricateSub
d_extricateSub_122 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_extricateSub_122 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Vec_28
d_extricateSub_122 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4
v2
  = case T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1 of
      T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4
        -> T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
MAlonzo.Code.Data.Vec.Base.C_'91''93'_32
      MAlonzo.Code.Type.C__'44''8902'__6 T_Ctx'8902'_2
v3 T_Kind_476
v4
        -> (T_Vec_28 -> T_Vec_28 -> T_Vec_28) -> Any -> Any -> T_Vec_28
forall a b. a -> b
coe
             T_Vec_28 -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du__'43''43'__188
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
 -> T_Vec_28)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Vec_28
d_extricateSub_122 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v3)
                ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v5 Any
v6 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4
v2 Any
v5 ((T__'8715''8902'__14 -> T__'8715''8902'__14) -> Any -> Any
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.C_S_18 Any
v6))))
             ((Any -> T_Vec_28) -> Any -> Any
forall a b. a -> b
coe
                Any -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_'91'_'93'_438
                ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                   T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
d_extricateNf'8902'_26 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v4)
                   ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476 -> Any -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4
v2 T_Kind_476
v4 (T__'8715''8902'__14 -> Any
forall a b. a -> b
coe T__'8715''8902'__14
MAlonzo.Code.Type.C_Z_16))))
      T_Ctx'8902'_2
_ -> T_Vec_28
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.Extrication.extricate
d_extricate_140 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Algorithmic.T_Ctx_2 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Scoped.T_ScopedTm_522
d_extricate_140 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
d_extricate_140 T_Ctx'8902'_2
v0 T_Ctx_2
v1 T__'8866'Nf'8902'__4
v2 T__'8866'__168
v3
  = case T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v3 of
      MAlonzo.Code.Algorithmic.C_'96'_174 T__'8715'__16
v5
        -> (T_WeirdFin_56 -> T_ScopedTm_522) -> Any -> T_ScopedTm_522
forall a b. a -> b
coe
             T_WeirdFin_56 -> T_ScopedTm_522
MAlonzo.Code.Scoped.C_'96'_528
             ((T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8715'__16 -> T_WeirdFin_56)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Ctx_2 -> T__'8715'__16 -> T_WeirdFin_56
du_extricateVar_110 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
v1) (T__'8715'__16 -> Any
forall a b. a -> b
coe T__'8715'__16
v5))
      MAlonzo.Code.Algorithmic.C_ƛ_180 T__'8866'__168
v6
        -> case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2 of
             MAlonzo.Code.Type.BetaNormal.C__'8658'__16 T__'8866'Nf'8902'__4
v8 T__'8866'Nf'8902'__4
v9
               -> (T_ScopedTy_14 -> T_ScopedTm_522 -> T_ScopedTm_522)
-> Any -> Any -> T_ScopedTm_522
forall a b. a -> b
coe
                    T_ScopedTy_14 -> T_ScopedTm_522 -> T_ScopedTm_522
MAlonzo.Code.Scoped.C_ƛ_534
                    ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
d_extricateNf'8902'_26 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)
                       (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v8))
                    ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
d_extricate_140 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                       ((T_Ctx_2 -> T__'8866'Nf'8902'__4 -> T_Ctx_2)
-> T_Ctx_2 -> T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T_Ctx_2 -> T__'8866'Nf'8902'__4 -> T_Ctx_2
MAlonzo.Code.Algorithmic.C__'44'__12 T_Ctx_2
v1 T__'8866'Nf'8902'__4
v8) (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v9) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v6))
             T__'8866'Nf'8902'__4
_ -> T_ScopedTm_522
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Algorithmic.C__'183'__186 T__'8866'Nf'8902'__4
v4 T__'8866'__168
v6 T__'8866'__168
v7
        -> (T_ScopedTm_522 -> T_ScopedTm_522 -> T_ScopedTm_522)
-> Any -> Any -> T_ScopedTm_522
forall a b. a -> b
coe
             T_ScopedTm_522 -> T_ScopedTm_522 -> T_ScopedTm_522
MAlonzo.Code.Scoped.C__'183'__536
             ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
d_extricate_140 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
v1)
                ((T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C__'8658'__16 T__'8866'Nf'8902'__4
v4 T__'8866'Nf'8902'__4
v2) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v6))
             ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
d_extricate_140 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
v1) (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v4) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v7))
      MAlonzo.Code.Algorithmic.C_Λ_192 T__'8866'__168
v6
        -> case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2 of
             MAlonzo.Code.Type.BetaNormal.C_Π_14 T_Kind_476
v8 T__'8866'Nf'8902'__4
v9
               -> (T_Kind_476 -> T_ScopedTm_522 -> T_ScopedTm_522)
-> Any -> Any -> T_ScopedTm_522
forall a b. a -> b
coe
                    T_Kind_476 -> T_ScopedTm_522 -> T_ScopedTm_522
MAlonzo.Code.Scoped.C_Λ_530 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v8)
                    ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
d_extricate_140
                       ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2) -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v8))
                       ((T_Ctx_2 -> T_Ctx_2) -> T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2 -> T_Ctx_2
MAlonzo.Code.Algorithmic.C__'44''8902'__8 T_Ctx_2
v1) (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v9)
                       (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v6))
             T__'8866'Nf'8902'__4
_ -> T_ScopedTm_522
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Algorithmic.C__'183''8902'_'47'__202 T_Kind_476
v4 T__'8866'Nf'8902'__4
v6 T__'8866'__168
v7 T__'8866'Nf'8902'__4
v8
        -> (T_ScopedTm_522 -> T_ScopedTy_14 -> T_ScopedTm_522)
-> Any -> Any -> T_ScopedTm_522
forall a b. a -> b
coe
             T_ScopedTm_522 -> T_ScopedTy_14 -> T_ScopedTm_522
MAlonzo.Code.Scoped.C__'183''8902'__532
             ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
d_extricate_140 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
v1)
                ((T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_Π_14 T_Kind_476
v4 T__'8866'Nf'8902'__4
v6) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v7))
             ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
d_extricateNf'8902'_26 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v4) (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v8))
      MAlonzo.Code.Algorithmic.C_wrap_210 T__'8866'__168
v7
        -> case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2 of
             MAlonzo.Code.Type.BetaNormal.C_μ_24 T_Kind_476
v9 T__'8866'Nf'8902'__4
v10 T__'8866'Nf'8902'__4
v11
               -> (T_ScopedTy_14
 -> T_ScopedTy_14 -> T_ScopedTm_522 -> T_ScopedTm_522)
-> Any -> Any -> Any -> T_ScopedTm_522
forall a b. a -> b
coe
                    T_ScopedTy_14 -> T_ScopedTy_14 -> T_ScopedTm_522 -> T_ScopedTm_522
MAlonzo.Code.Scoped.C_wrap_546
                    ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
d_extricateNf'8902'_26 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                       ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                          T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482
                          ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                             T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                             (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                          ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                             T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                             (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
                       (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v10))
                    ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
d_extricateNf'8902'_26 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9) (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v11))
                    ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
d_extricate_140 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
v1)
                       ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866'Nf'8902'__4)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                          T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNBE.d_nf_258 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                          (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)
                          ((T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> T_Kind_476 -> Any -> T__'8866''8902'__20 -> Any
forall a b. a -> b
coe
                             T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30 T_Kind_476
v9
                             ((T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> Any -> T__'8866''8902'__20 -> Any -> Any
forall a b. a -> b
coe
                                T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30
                                ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                   T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                   (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                                (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.d_embNf_128
                                   (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                                   ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> Any -> Any -> T_Kind_476
forall a b. a -> b
coe
                                      T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482
                                      ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                         T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                         (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                                      ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                         T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                         (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
                                   (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v10))
                                ((T__'8866''8902'__20 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe
                                   T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_ƛ_28
                                   ((T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> T_Kind_476 -> T__'8866''8902'__20 -> Any -> Any
forall a b. a -> b
coe
                                      T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C_μ_32 T_Kind_476
v9
                                      (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.d_embNf_128
                                         ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> Any -> Any -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9))
                                         ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> Any -> Any -> T_Kind_476
forall a b. a -> b
coe
                                            T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482
                                            ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                               T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                               (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                                            ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                               T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                               (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
                                         ((T_Ctx'8902'_2
 -> T_Kind_476
 -> T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4)
-> T_Ctx'8902'_2
-> Any
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
                                            T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.d_weakenNf_122 T_Ctx'8902'_2
v0
                                            ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                               T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482
                                               ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                  T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                                  (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                                               ((T_Kind_476 -> T_Kind_476 -> T_Kind_476) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                  T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v9)
                                                  (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
                                            T_Kind_476
v9 T__'8866'Nf'8902'__4
v10))
                                      ((T__'8715''8902'__14 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe
                                         T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22
                                         (T__'8715''8902'__14 -> Any
forall a b. a -> b
coe T__'8715''8902'__14
MAlonzo.Code.Type.C_Z_16)))))
                             (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.d_embNf_128
                                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v9) (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v11))))
                       (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v7))
             T__'8866'Nf'8902'__4
_ -> T_ScopedTm_522
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Algorithmic.C_unwrap_220 T_Kind_476
v4 T__'8866'Nf'8902'__4
v6 T__'8866'Nf'8902'__4
v7 T__'8866'__168
v8
        -> (T_ScopedTm_522 -> T_ScopedTm_522) -> Any -> T_ScopedTm_522
forall a b. a -> b
coe
             T_ScopedTm_522 -> T_ScopedTm_522
MAlonzo.Code.Scoped.C_unwrap_548
             ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
d_extricate_140 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
v1)
                ((T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> Any
forall a b. a -> b
coe T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_μ_24 T_Kind_476
v4 T__'8866'Nf'8902'__4
v6 T__'8866'Nf'8902'__4
v7) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v8))
      MAlonzo.Code.Algorithmic.C_constr_230 T_Fin_10
v5 [T__'8866'Nf'8902'__4]
v7 T_IList_302
v9
        -> case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2 of
             MAlonzo.Code.Type.BetaNormal.C_SOP_28 Integer
v11 T_Vec_28
v12
               -> (T_ScopedTy_14
 -> Integer -> T_List_382 T_ScopedTm_522 -> T_ScopedTm_522)
-> Any -> Any -> Any -> T_ScopedTm_522
forall a b. a -> b
coe
                    T_ScopedTy_14
-> Integer -> T_List_382 T_ScopedTm_522 -> T_ScopedTm_522
MAlonzo.Code.Scoped.C_constr_556
                    ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
d_extricateNf'8902'_26 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)
                       ((Integer -> T_Vec_28 -> T__'8866'Nf'8902'__4)
-> Integer -> T_Vec_28 -> Any
forall a b. a -> b
coe Integer -> T_Vec_28 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_SOP_28 Integer
v11 T_Vec_28
v12))
                    ((T_Fin_10 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> Integer
MAlonzo.Code.Data.Fin.Base.du_toℕ_18 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v5))
                    ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> [T__'8866'Nf'8902'__4]
 -> T_IList_302
 -> T_List_382 T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Ctx'8902'_2
-> T_Ctx_2
-> [T__'8866'Nf'8902'__4]
-> T_IList_302
-> T_List_382 T_ScopedTm_522
d_extricate'45'ConstrArgs_148 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
v1)
                       ((T_Vec_28 -> T_Fin_10 -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe T_Vec_28 -> T_Fin_10 -> Any
MAlonzo.Code.Data.Vec.Base.du_lookup_82 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v12) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v5))
                       (T_IList_302 -> Any
forall a b. a -> b
coe T_IList_302
v9))
             T__'8866'Nf'8902'__4
_ -> T_ScopedTm_522
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Algorithmic.C_case_242 Integer
v4 T_Vec_28
v5 T__'8866'__168
v7 T_Cases_162
v8
        -> (T_ScopedTy_14
 -> T_ScopedTm_522 -> T_List_382 T_ScopedTm_522 -> T_ScopedTm_522)
-> Any -> Any -> Any -> T_ScopedTm_522
forall a b. a -> b
coe
             T_ScopedTy_14
-> T_ScopedTm_522 -> T_List_382 T_ScopedTm_522 -> T_ScopedTm_522
MAlonzo.Code.Scoped.C_case_564
             ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
d_extricateNf'8902'_26 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)
                (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2))
             ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
d_extricate_140 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
v1)
                ((Integer -> T_Vec_28 -> T__'8866'Nf'8902'__4)
-> Integer -> T_Vec_28 -> Any
forall a b. a -> b
coe Integer -> T_Vec_28 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_SOP_28 Integer
v4 T_Vec_28
v5) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v7))
             ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T_Vec_28
 -> T_Cases_162
 -> T_List_382 T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Vec_28
-> T_Cases_162
-> T_List_382 T_ScopedTm_522
du_extricate'45'Cases_166 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
v1) (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2) (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v5)
                (T_Cases_162 -> Any
forall a b. a -> b
coe T_Cases_162
v8))
      MAlonzo.Code.Algorithmic.C_con_248 T__'8866'Nf'8902'__4
v4 Any
v6
        -> (T_TmCon_198 -> T_ScopedTm_522) -> Any -> T_ScopedTm_522
forall a b. a -> b
coe
             T_TmCon_198 -> T_ScopedTm_522
MAlonzo.Code.Scoped.C_con_538
             ((T__'8866''9839'_4 -> Any -> T_TmCon_198) -> Any -> Any -> Any
forall a b. a -> b
coe
                T__'8866''9839'_4 -> Any -> T_TmCon_198
MAlonzo.Code.RawU.C_tmCon_202
                ((T__'8866'Nf'8902'__4 -> T__'8866''9839'_4) -> Any -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4 -> T__'8866''9839'_4
MAlonzo.Code.Algorithmic.d_ty2sty_64 (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v4)) (Any -> Any
forall a b. a -> b
coe Any
v6))
      MAlonzo.Code.Algorithmic.C_builtin_'47'__254 T_Builtin_2
v5
        -> (T_Builtin_2 -> T_ScopedTm_522) -> Any -> T_ScopedTm_522
forall a b. a -> b
coe T_Builtin_2 -> T_ScopedTm_522
MAlonzo.Code.Scoped.C_builtin_544 (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v5)
      T__'8866'__168
MAlonzo.Code.Algorithmic.C_error_258
        -> (T_ScopedTy_14 -> T_ScopedTm_522) -> Any -> T_ScopedTm_522
forall a b. a -> b
coe
             T_ScopedTy_14 -> T_ScopedTm_522
MAlonzo.Code.Scoped.C_error_540
             ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
d_extricateNf'8902'_26 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)
                (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2))
      T__'8866'__168
_ -> T_ScopedTm_522
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.Extrication.extricate-ConstrArgs
d_extricate'45'ConstrArgs_148 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Algorithmic.T_Ctx_2 ->
  [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
  MAlonzo.Code.Utils.List.T_IList_302 ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Scoped.T_ScopedTm_522
d_extricate'45'ConstrArgs_148 :: T_Ctx'8902'_2
-> T_Ctx_2
-> [T__'8866'Nf'8902'__4]
-> T_IList_302
-> T_List_382 T_ScopedTm_522
d_extricate'45'ConstrArgs_148 T_Ctx'8902'_2
v0 T_Ctx_2
v1 [T__'8866'Nf'8902'__4]
v2 T_IList_302
v3
  = case T_IList_302 -> T_IList_302
forall a b. a -> b
coe T_IList_302
v3 of
      T_IList_302
MAlonzo.Code.Utils.List.C_'91''93'_308
        -> [Any] -> T_List_382 T_ScopedTm_522
forall a b. a -> b
coe [Any]
forall {a}. [a]
MAlonzo.Code.Utils.C_'91''93'_386
      MAlonzo.Code.Utils.List.C__'8759'__314 Any
v6 T_IList_302
v7
        -> case [T__'8866'Nf'8902'__4] -> [Any]
forall a b. a -> b
coe [T__'8866'Nf'8902'__4]
v2 of
             (:) Any
v8 [Any]
v9
               -> (Any -> [Any] -> [Any]) -> Any -> Any -> T_List_382 T_ScopedTm_522
forall a b. a -> b
coe
                    Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
                    ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
d_extricate_140 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
v1) (Any -> Any
forall a b. a -> b
coe Any
v8) (Any -> Any
forall a b. a -> b
coe Any
v6))
                    ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> [T__'8866'Nf'8902'__4]
 -> T_IList_302
 -> T_List_382 T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Ctx'8902'_2
-> T_Ctx_2
-> [T__'8866'Nf'8902'__4]
-> T_IList_302
-> T_List_382 T_ScopedTm_522
d_extricate'45'ConstrArgs_148 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
v1) ([Any] -> Any
forall a b. a -> b
coe [Any]
v9) (T_IList_302 -> Any
forall a b. a -> b
coe T_IList_302
v7))
             [Any]
_ -> T_List_382 T_ScopedTm_522
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_IList_302
_ -> T_List_382 T_ScopedTm_522
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Scoped.Extrication.extricate-Cases
d_extricate'45'Cases_166 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Algorithmic.T_Ctx_2 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  Integer ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Algorithmic.T_Cases_162 ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Scoped.T_ScopedTm_522
d_extricate'45'Cases_166 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> Integer
-> T_Vec_28
-> T_Cases_162
-> T_List_382 T_ScopedTm_522
d_extricate'45'Cases_166 T_Ctx'8902'_2
v0 T_Ctx_2
v1 T__'8866'Nf'8902'__4
v2 ~Integer
v3 T_Vec_28
v4 T_Cases_162
v5
  = T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Vec_28
-> T_Cases_162
-> T_List_382 T_ScopedTm_522
du_extricate'45'Cases_166 T_Ctx'8902'_2
v0 T_Ctx_2
v1 T__'8866'Nf'8902'__4
v2 T_Vec_28
v4 T_Cases_162
v5
du_extricate'45'Cases_166 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Algorithmic.T_Ctx_2 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Algorithmic.T_Cases_162 ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Scoped.T_ScopedTm_522
du_extricate'45'Cases_166 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Vec_28
-> T_Cases_162
-> T_List_382 T_ScopedTm_522
du_extricate'45'Cases_166 T_Ctx'8902'_2
v0 T_Ctx_2
v1 T__'8866'Nf'8902'__4
v2 T_Vec_28
v3 T_Cases_162
v4
  = case T_Cases_162 -> T_Cases_162
forall a b. a -> b
coe T_Cases_162
v4 of
      T_Cases_162
MAlonzo.Code.Algorithmic.C_'91''93'_268
        -> [Any] -> T_List_382 T_ScopedTm_522
forall a b. a -> b
coe [Any]
forall {a}. [a]
MAlonzo.Code.Utils.C_'91''93'_386
      MAlonzo.Code.Algorithmic.C__'8759'__280 T__'8866'__168
v8 T_Cases_162
v9
        -> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v3 of
             MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v11 T_Vec_28
v12
               -> (Any -> [Any] -> [Any]) -> Any -> Any -> T_List_382 T_ScopedTm_522
forall a b. a -> b
coe
                    Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
                    ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
d_extricate_140 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
v1)
                       ((T__'8866'Nf'8902'__4
 -> [T__'8866'Nf'8902'__4] -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4 -> Any -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
-> [T__'8866'Nf'8902'__4] -> T__'8866'Nf'8902'__4
MAlonzo.Code.Algorithmic.du_mkCaseType_146 T__'8866'Nf'8902'__4
v2 Any
v11) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v8))
                    ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T_Vec_28
 -> T_Cases_162
 -> T_List_382 T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Vec_28
-> T_Cases_162
-> T_List_382 T_ScopedTm_522
du_extricate'45'Cases_166 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
v1) (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2) (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v12)
                       (T_Cases_162 -> Any
forall a b. a -> b
coe T_Cases_162
v9))
             T_Vec_28
_ -> T_List_382 T_ScopedTm_522
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Cases_162
_ -> T_List_382 T_ScopedTm_522
forall a. a
MAlonzo.RTE.mazUnreachableError