{-# 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.Data.Fin.Base 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.Equality
import qualified MAlonzo.Code.Agda.Builtin.Nat
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Algebra.Definitions.RawMagma
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core

-- Data.Fin.Base.Fin
d_Fin_10 :: p -> ()
d_Fin_10 p
a0 = ()
data T_Fin_10 = C_zero_12 | C_suc_16 T_Fin_10
-- Data.Fin.Base.toℕ
d_toℕ_18 :: Integer -> T_Fin_10 -> Integer
d_toℕ_18 :: Integer -> T_Fin_10 -> Integer
d_toℕ_18 ~Integer
v0 T_Fin_10
v1 = T_Fin_10 -> Integer
du_toℕ_18 T_Fin_10
v1
du_toℕ_18 :: T_Fin_10 -> Integer
du_toℕ_18 :: T_Fin_10 -> Integer
du_toℕ_18 T_Fin_10
v0
  = case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0 of
      T_Fin_10
C_zero_12 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      C_suc_16 T_Fin_10
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_Fin_10 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> Integer
du_toℕ_18 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v2))
      T_Fin_10
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.Fin′
d_Fin'8242'_22 :: Integer -> T_Fin_10 -> ()
d_Fin'8242'_22 :: Integer -> T_Fin_10 -> ()
d_Fin'8242'_22 = Integer -> T_Fin_10 -> ()
forall a. a
erased
-- Data.Fin.Base.cast
d_cast_26 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T_Fin_10 -> T_Fin_10
d_cast_26 :: Integer -> Integer -> T__'8801'__12 -> T_Fin_10 -> T_Fin_10
d_cast_26 Integer
v0 ~Integer
v1 ~T__'8801'__12
v2 T_Fin_10
v3 = Integer -> T_Fin_10 -> T_Fin_10
du_cast_26 Integer
v0 T_Fin_10
v3
du_cast_26 :: Integer -> T_Fin_10 -> T_Fin_10
du_cast_26 :: Integer -> T_Fin_10 -> T_Fin_10
du_cast_26 Integer
v0 T_Fin_10
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1
      Integer
_ -> case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
             T_Fin_10
C_zero_12 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
C_zero_12
             C_suc_16 T_Fin_10
v3
               -> (T_Fin_10 -> T_Fin_10) -> Any -> T_Fin_10
forall a b. a -> b
coe
                    T_Fin_10 -> T_Fin_10
C_suc_16
                    ((Integer -> T_Fin_10 -> T_Fin_10) -> Any -> Any -> Any
forall a b. a -> b
coe
                       Integer -> T_Fin_10 -> T_Fin_10
du_cast_26
                       ((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v0 (Integer
1 :: Integer))
                       (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v3))
             T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.fromℕ
d_fromℕ_48 :: Integer -> T_Fin_10
d_fromℕ_48 :: Integer -> T_Fin_10
d_fromℕ_48 Integer
v0
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
C_zero_12
      Integer
_ -> let v1 :: Integer
v1 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T_Fin_10
forall a b. a -> b
coe ((T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16 (Integer -> T_Fin_10
d_fromℕ_48 (Integer -> Integer
forall a b. a -> b
coe Integer
v1)))
-- Data.Fin.Base.fromℕ<
d_fromℕ'60'_52 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22 -> T_Fin_10
d_fromℕ'60'_52 :: Integer -> Integer -> T__'8804'__22 -> T_Fin_10
d_fromℕ'60'_52 Integer
v0 ~Integer
v1 ~T__'8804'__22
v2 = Integer -> T_Fin_10
du_fromℕ'60'_52 Integer
v0
du_fromℕ'60'_52 :: Integer -> T_Fin_10
du_fromℕ'60'_52 :: Integer -> T_Fin_10
du_fromℕ'60'_52 Integer
v0
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
C_zero_12
      Integer
_ -> let v1 :: Integer
v1 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T_Fin_10
forall a b. a -> b
coe ((T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16 ((Integer -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_10
du_fromℕ'60'_52 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
-- Data.Fin.Base.fromℕ<″
d_fromℕ'60''8243'_62 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__28 ->
  T_Fin_10
d_fromℕ'60''8243'_62 :: Integer -> Integer -> T__'8739''737'__28 -> T_Fin_10
d_fromℕ'60''8243'_62 Integer
v0 ~Integer
v1 ~T__'8739''737'__28
v2 = Integer -> T_Fin_10
du_fromℕ'60''8243'_62 Integer
v0
du_fromℕ'60''8243'_62 :: Integer -> T_Fin_10
du_fromℕ'60''8243'_62 :: Integer -> T_Fin_10
du_fromℕ'60''8243'_62 Integer
v0
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
C_zero_12
      Integer
_ -> let v1 :: Integer
v1 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T_Fin_10
forall a b. a -> b
coe ((T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16 ((Integer -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_10
du_fromℕ'60''8243'_62 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
-- Data.Fin.Base._↑ˡ_
d__'8593''737'__72 :: Integer -> T_Fin_10 -> Integer -> T_Fin_10
d__'8593''737'__72 :: Integer -> T_Fin_10 -> Integer -> T_Fin_10
d__'8593''737'__72 ~Integer
v0 T_Fin_10
v1 ~Integer
v2 = T_Fin_10 -> T_Fin_10
du__'8593''737'__72 T_Fin_10
v1
du__'8593''737'__72 :: T_Fin_10 -> T_Fin_10
du__'8593''737'__72 :: T_Fin_10 -> T_Fin_10
du__'8593''737'__72 T_Fin_10
v0 = T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0
-- Data.Fin.Base._↑ʳ_
d__'8593''691'__84 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d__'8593''691'__84 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d__'8593''691'__84 ~Integer
v0 Integer
v1 T_Fin_10
v2 = Integer -> T_Fin_10 -> T_Fin_10
du__'8593''691'__84 Integer
v1 T_Fin_10
v2
du__'8593''691'__84 :: Integer -> T_Fin_10 -> T_Fin_10
du__'8593''691'__84 :: Integer -> T_Fin_10 -> T_Fin_10
du__'8593''691'__84 Integer
v0 T_Fin_10
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T_Fin_10
forall a b. a -> b
coe ((T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16 ((Integer -> T_Fin_10 -> T_Fin_10) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_10 -> T_Fin_10
du__'8593''691'__84 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v1)))
-- Data.Fin.Base.reduce≥
d_reduce'8805'_94 ::
  Integer ->
  Integer ->
  T_Fin_10 -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22 -> T_Fin_10
d_reduce'8805'_94 :: Integer -> Integer -> T_Fin_10 -> T__'8804'__22 -> T_Fin_10
d_reduce'8805'_94 Integer
v0 ~Integer
v1 T_Fin_10
v2 ~T__'8804'__22
v3 = Integer -> T_Fin_10 -> T_Fin_10
du_reduce'8805'_94 Integer
v0 T_Fin_10
v2
du_reduce'8805'_94 :: Integer -> T_Fin_10 -> T_Fin_10
du_reduce'8805'_94 :: Integer -> T_Fin_10 -> T_Fin_10
du_reduce'8805'_94 Integer
v0 T_Fin_10
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T_Fin_10
forall a b. a -> b
coe
             (case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
                C_suc_16 T_Fin_10
v4 -> (Integer -> T_Fin_10 -> T_Fin_10) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_10 -> T_Fin_10
du_reduce'8805'_94 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v4)
                T_Fin_10
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Fin.Base.inject
d_inject_104 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_inject_104 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_inject_104 ~Integer
v0 T_Fin_10
v1 T_Fin_10
v2 = T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_inject_104 T_Fin_10
v1 T_Fin_10
v2
du_inject_104 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_inject_104 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_inject_104 T_Fin_10
v0 T_Fin_10
v1
  = case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0 of
      C_suc_16 T_Fin_10
v3
        -> case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
             T_Fin_10
C_zero_12 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
C_zero_12
             C_suc_16 T_Fin_10
v5 -> (T_Fin_10 -> T_Fin_10) -> Any -> T_Fin_10
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16 ((T_Fin_10 -> T_Fin_10 -> T_Fin_10) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_inject_104 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v3) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v5))
             T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.inject!
d_inject'33'_114 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_inject'33'_114 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_inject'33'_114 ~Integer
v0 T_Fin_10
v1 T_Fin_10
v2 = T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_inject'33'_114 T_Fin_10
v1 T_Fin_10
v2
du_inject'33'_114 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_inject'33'_114 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_inject'33'_114 T_Fin_10
v0 T_Fin_10
v1
  = case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0 of
      C_suc_16 T_Fin_10
v3
        -> case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
             T_Fin_10
C_zero_12 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
C_zero_12
             C_suc_16 T_Fin_10
v5
               -> (T_Fin_10 -> T_Fin_10) -> Any -> T_Fin_10
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16 ((T_Fin_10 -> T_Fin_10 -> T_Fin_10) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_inject'33'_114 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v3) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v5))
             T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.inject₁
d_inject'8321'_118 :: Integer -> T_Fin_10 -> T_Fin_10
d_inject'8321'_118 :: Integer -> T_Fin_10 -> T_Fin_10
d_inject'8321'_118 ~Integer
v0 T_Fin_10
v1 = T_Fin_10 -> T_Fin_10
du_inject'8321'_118 T_Fin_10
v1
du_inject'8321'_118 :: T_Fin_10 -> T_Fin_10
du_inject'8321'_118 :: T_Fin_10 -> T_Fin_10
du_inject'8321'_118 T_Fin_10
v0 = T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0
-- Data.Fin.Base.inject≤
d_inject'8804'_122 ::
  Integer ->
  Integer ->
  T_Fin_10 -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22 -> T_Fin_10
d_inject'8804'_122 :: Integer -> Integer -> T_Fin_10 -> T__'8804'__22 -> T_Fin_10
d_inject'8804'_122 ~Integer
v0 ~Integer
v1 T_Fin_10
v2 ~T__'8804'__22
v3 = T_Fin_10 -> T_Fin_10
du_inject'8804'_122 T_Fin_10
v2
du_inject'8804'_122 :: T_Fin_10 -> T_Fin_10
du_inject'8804'_122 :: T_Fin_10 -> T_Fin_10
du_inject'8804'_122 T_Fin_10
v0 = T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0
-- Data.Fin.Base.lower₁
d_lower'8321'_130 ::
  Integer ->
  T_Fin_10 ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  T_Fin_10
d_lower'8321'_130 :: Integer
-> T_Fin_10 -> (T__'8801'__12 -> T_Irrelevant_20) -> T_Fin_10
d_lower'8321'_130 Integer
v0 T_Fin_10
v1 ~T__'8801'__12 -> T_Irrelevant_20
v2 = Integer -> T_Fin_10 -> T_Fin_10
du_lower'8321'_130 Integer
v0 T_Fin_10
v1
du_lower'8321'_130 :: Integer -> T_Fin_10 -> T_Fin_10
du_lower'8321'_130 :: Integer -> T_Fin_10 -> T_Fin_10
du_lower'8321'_130 Integer
v0 T_Fin_10
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> (Any -> Any -> Any) -> Any -> Any -> T_Fin_10
forall a b. a -> b
coe
             Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v1)
             (((Any -> T_Irrelevant_20) -> Any) -> Any -> Any
forall a b. a -> b
coe
                (Any -> T_Irrelevant_20) -> Any
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                Any
forall a. a
erased)
      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_Fin_10
forall a b. a -> b
coe
             (case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
                T_Fin_10
C_zero_12 -> T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
C_zero_12
                C_suc_16 T_Fin_10
v4
                  -> (T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16 ((Integer -> T_Fin_10 -> T_Fin_10) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_10 -> T_Fin_10
du_lower'8321'_130 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v4))
                T_Fin_10
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Fin.Base.lower
d_lower_144 ::
  Integer ->
  Integer ->
  T_Fin_10 -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22 -> T_Fin_10
d_lower_144 :: Integer -> Integer -> T_Fin_10 -> T__'8804'__22 -> T_Fin_10
d_lower_144 ~Integer
v0 ~Integer
v1 T_Fin_10
v2 ~T__'8804'__22
v3 = T_Fin_10 -> T_Fin_10
du_lower_144 T_Fin_10
v2
du_lower_144 :: T_Fin_10 -> T_Fin_10
du_lower_144 :: T_Fin_10 -> T_Fin_10
du_lower_144 T_Fin_10
v0 = T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0
-- Data.Fin.Base.strengthen
d_strengthen_158 :: Integer -> T_Fin_10 -> T_Fin_10
d_strengthen_158 :: Integer -> T_Fin_10 -> T_Fin_10
d_strengthen_158 ~Integer
v0 T_Fin_10
v1 = T_Fin_10 -> T_Fin_10
du_strengthen_158 T_Fin_10
v1
du_strengthen_158 :: T_Fin_10 -> T_Fin_10
du_strengthen_158 :: T_Fin_10 -> T_Fin_10
du_strengthen_158 T_Fin_10
v0 = T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0
-- Data.Fin.Base.splitAt
d_splitAt_166 ::
  Integer ->
  Integer -> T_Fin_10 -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_splitAt_166 :: Integer -> Integer -> T_Fin_10 -> T__'8846'__30
d_splitAt_166 Integer
v0 ~Integer
v1 T_Fin_10
v2 = Integer -> T_Fin_10 -> T__'8846'__30
du_splitAt_166 Integer
v0 T_Fin_10
v2
du_splitAt_166 ::
  Integer -> T_Fin_10 -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_splitAt_166 :: Integer -> T_Fin_10 -> T__'8846'__30
du_splitAt_166 Integer
v0 T_Fin_10
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> (Any -> T__'8846'__30) -> Any -> T__'8846'__30
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v1)
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           Any -> T__'8846'__30
forall a b. a -> b
coe
             (case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
                T_Fin_10
C_zero_12
                  -> (Any -> T__'8846'__30) -> Any -> Any
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
C_zero_12)
                C_suc_16 T_Fin_10
v4
                  -> ((Any -> Any) -> T__'8846'__30 -> T__'8846'__30)
-> Any -> Any -> Any
forall a b. a -> b
coe
                       (Any -> Any) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map'8321'_90 ((T_Fin_10 -> T_Fin_10) -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16)
                       ((Integer -> T_Fin_10 -> T__'8846'__30) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_10 -> T__'8846'__30
du_splitAt_166 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v4))
                T_Fin_10
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Fin.Base.join
d_join_180 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Fin_10
d_join_180 :: Integer -> Integer -> T__'8846'__30 -> T_Fin_10
d_join_180 Integer
v0 ~Integer
v1 = Integer -> T__'8846'__30 -> T_Fin_10
du_join_180 Integer
v0
du_join_180 ::
  Integer -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Fin_10
du_join_180 :: Integer -> T__'8846'__30 -> T_Fin_10
du_join_180 Integer
v0
  = ((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> Any)
-> (Any -> Any) -> Any -> T__'8846'__30 -> T_Fin_10
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> Any
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93''8242'_66 (\ Any
v1 -> Any
v1)
      ((Integer -> T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_10 -> T_Fin_10
du__'8593''691'__84 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
-- Data.Fin.Base.quotRem
d_quotRem_192 ::
  Integer ->
  Integer -> T_Fin_10 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_quotRem_192 :: Integer -> Integer -> T_Fin_10 -> T_Σ_14
d_quotRem_192 ~Integer
v0 Integer
v1 T_Fin_10
v2 = Integer -> T_Fin_10 -> T_Σ_14
du_quotRem_192 Integer
v1 T_Fin_10
v2
du_quotRem_192 ::
  Integer -> T_Fin_10 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_quotRem_192 :: Integer -> T_Fin_10 -> T_Σ_14
du_quotRem_192 Integer
v0 T_Fin_10
v1
  = ((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> Any)
-> (Any -> Any) -> (Any -> Any) -> Any -> T_Σ_14
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> Any
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93''8242'_66
      (\ Any
v2 ->
         (Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
           Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (Any -> Any
forall a b. a -> b
coe Any
v2)
           (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
C_zero_12))
      (\ Any
v2 ->
         ((Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14)
-> (Any -> Any) -> Any -> Any
forall a b. a -> b
coe
           (Any -> Any -> Any) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map'8322'_150
           (\ Any
v3 -> (T_Fin_10 -> T_Fin_10) -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16) ((Integer -> T_Fin_10 -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_10 -> T_Σ_14
du_quotRem_192 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Any -> Any
forall a b. a -> b
coe Any
v2)))
      ((Integer -> T_Fin_10 -> T__'8846'__30) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_10 -> T__'8846'__30
du_splitAt_166 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v1))
-- Data.Fin.Base.remQuot
d_remQuot_204 ::
  Integer ->
  Integer -> T_Fin_10 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_remQuot_204 :: Integer -> Integer -> T_Fin_10 -> T_Σ_14
d_remQuot_204 ~Integer
v0 Integer
v1 T_Fin_10
v2 = Integer -> T_Fin_10 -> T_Σ_14
du_remQuot_204 Integer
v1 T_Fin_10
v2
du_remQuot_204 ::
  Integer -> T_Fin_10 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_remQuot_204 :: Integer -> T_Fin_10 -> T_Σ_14
du_remQuot_204 Integer
v0 T_Fin_10
v1
  = (T_Σ_14 -> T_Σ_14) -> Any -> T_Σ_14
forall a b. a -> b
coe
      T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_swap_370
      ((Integer -> T_Fin_10 -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_10 -> T_Σ_14
du_quotRem_192 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v1))
-- Data.Fin.Base.quotient
d_quotient_210 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d_quotient_210 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d_quotient_210 ~Integer
v0 Integer
v1 T_Fin_10
v2 = Integer -> T_Fin_10 -> T_Fin_10
du_quotient_210 Integer
v1 T_Fin_10
v2
du_quotient_210 :: Integer -> T_Fin_10 -> T_Fin_10
du_quotient_210 :: Integer -> T_Fin_10 -> T_Fin_10
du_quotient_210 Integer
v0 T_Fin_10
v1
  = (T_Σ_14 -> Any) -> Any -> T_Fin_10
forall a b. a -> b
coe
      T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
      ((Integer -> T_Fin_10 -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_10 -> T_Σ_14
du_remQuot_204 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v1))
-- Data.Fin.Base.remainder
d_remainder_216 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d_remainder_216 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d_remainder_216 ~Integer
v0 Integer
v1 T_Fin_10
v2 = Integer -> T_Fin_10 -> T_Fin_10
du_remainder_216 Integer
v1 T_Fin_10
v2
du_remainder_216 :: Integer -> T_Fin_10 -> T_Fin_10
du_remainder_216 :: Integer -> T_Fin_10 -> T_Fin_10
du_remainder_216 Integer
v0 T_Fin_10
v1
  = (T_Σ_14 -> Any) -> Any -> T_Fin_10
forall a b. a -> b
coe
      T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
      ((Integer -> T_Fin_10 -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_10 -> T_Σ_14
du_remQuot_204 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v1))
-- Data.Fin.Base.combine
d_combine_222 ::
  Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_combine_222 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_combine_222 ~Integer
v0 Integer
v1 T_Fin_10
v2 T_Fin_10
v3 = Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_combine_222 Integer
v1 T_Fin_10
v2 T_Fin_10
v3
du_combine_222 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_combine_222 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_combine_222 Integer
v0 T_Fin_10
v1 T_Fin_10
v2
  = case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
      T_Fin_10
C_zero_12 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v2
      C_suc_16 T_Fin_10
v4
        -> (Integer -> T_Fin_10 -> T_Fin_10) -> Any -> Any -> T_Fin_10
forall a b. a -> b
coe
             Integer -> T_Fin_10 -> T_Fin_10
du__'8593''691'__84 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
             ((Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_combine_222 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v4) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v2))
      T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.finToFun
d_finToFun_238 ::
  Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_finToFun_238 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_finToFun_238 Integer
v0 Integer
v1 T_Fin_10
v2 T_Fin_10
v3
  = 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_Fin_10
forall a b. a -> b
coe
      (case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v3 of
         T_Fin_10
C_zero_12
           -> (Integer -> T_Fin_10 -> T_Fin_10) -> Any -> Any -> Any
forall a b. a -> b
coe
                Integer -> T_Fin_10 -> T_Fin_10
du_quotient_210
                ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'94'__276 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v2)
         C_suc_16 T_Fin_10
v6
           -> (Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_finToFun_238 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v4)
                ((Integer -> T_Fin_10 -> T_Fin_10) -> Any -> Any -> Any
forall a b. a -> b
coe
                   Integer -> T_Fin_10 -> T_Fin_10
du_remainder_216
                   ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'94'__276 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                   (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v2))
                (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v6)
         T_Fin_10
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Fin.Base.funToFin
d_funToFin_254 ::
  Integer -> Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10
d_funToFin_254 :: Integer -> Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10
d_funToFin_254 Integer
v0 Integer
v1 T_Fin_10 -> T_Fin_10
v2
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
C_zero_12
      Integer
_ -> let v3 :: Integer
v3 = 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_Fin_10
forall a b. a -> b
coe
             ((Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_combine_222
                ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'94'__276 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v3))
                ((T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
v2 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
C_zero_12))
                ((Integer -> Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                   Integer -> Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10
d_funToFin_254 (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
                   ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v4 -> (T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
v2 ((T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16 Any
v4)))))
-- Data.Fin.Base.fold
d_fold_272 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (Integer -> ()) ->
  Integer ->
  (Integer -> AgdaAny -> AgdaAny) ->
  (Integer -> AgdaAny) -> T_Fin_10 -> AgdaAny
d_fold_272 :: ()
-> (Integer -> ())
-> Integer
-> (Integer -> Any -> Any)
-> (Integer -> Any)
-> T_Fin_10
-> Any
d_fold_272 ~()
v0 ~Integer -> ()
v1 Integer
v2 Integer -> Any -> Any
v3 Integer -> Any
v4 T_Fin_10
v5 = Integer
-> (Integer -> Any -> Any) -> (Integer -> Any) -> T_Fin_10 -> Any
du_fold_272 Integer
v2 Integer -> Any -> Any
v3 Integer -> Any
v4 T_Fin_10
v5
du_fold_272 ::
  Integer ->
  (Integer -> AgdaAny -> AgdaAny) ->
  (Integer -> AgdaAny) -> T_Fin_10 -> AgdaAny
du_fold_272 :: Integer
-> (Integer -> Any -> Any) -> (Integer -> Any) -> T_Fin_10 -> Any
du_fold_272 Integer
v0 Integer -> Any -> Any
v1 Integer -> Any
v2 T_Fin_10
v3
  = case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v3 of
      T_Fin_10
C_zero_12
        -> let v5 :: Integer
v5 = 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 -> Any
forall a b. a -> b
coe ((Integer -> Any) -> Integer -> Any
forall a b. a -> b
coe Integer -> Any
v2 Integer
v5)
      C_suc_16 T_Fin_10
v5
        -> let v6 :: Integer
v6 = 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 -> Any
forall a b. a -> b
coe
             ((Integer -> Any -> Any) -> Integer -> Any -> Any
forall a b. a -> b
coe Integer -> Any -> Any
v1 Integer
v6 ((Integer
 -> (Integer -> Any -> Any) -> (Integer -> Any) -> T_Fin_10 -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer
-> (Integer -> Any -> Any) -> (Integer -> Any) -> T_Fin_10 -> Any
du_fold_272 (Integer -> Any
forall a b. a -> b
coe Integer
v6) ((Integer -> Any -> Any) -> Any
forall a b. a -> b
coe Integer -> Any -> Any
v1) ((Integer -> Any) -> Any
forall a b. a -> b
coe Integer -> Any
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v5)))
      T_Fin_10
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.fold′
d_fold'8242'_298 ::
  Integer ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (T_Fin_10 -> ()) ->
  (T_Fin_10 -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Fin_10 -> AgdaAny
d_fold'8242'_298 :: Integer
-> ()
-> (T_Fin_10 -> ())
-> (T_Fin_10 -> Any -> Any)
-> Any
-> T_Fin_10
-> Any
d_fold'8242'_298 ~Integer
v0 ~()
v1 ~T_Fin_10 -> ()
v2 T_Fin_10 -> Any -> Any
v3 Any
v4 T_Fin_10
v5 = (T_Fin_10 -> Any -> Any) -> Any -> T_Fin_10 -> Any
du_fold'8242'_298 T_Fin_10 -> Any -> Any
v3 Any
v4 T_Fin_10
v5
du_fold'8242'_298 ::
  (T_Fin_10 -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Fin_10 -> AgdaAny
du_fold'8242'_298 :: (T_Fin_10 -> Any -> Any) -> Any -> T_Fin_10 -> Any
du_fold'8242'_298 T_Fin_10 -> Any -> Any
v0 Any
v1 T_Fin_10
v2
  = case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v2 of
      T_Fin_10
C_zero_12 -> Any -> Any
forall a b. a -> b
coe Any
v1
      C_suc_16 T_Fin_10
v4
        -> (T_Fin_10 -> Any -> Any) -> T_Fin_10 -> Any -> Any
forall a b. a -> b
coe
             T_Fin_10 -> Any -> Any
v0 T_Fin_10
v4
             (((T_Fin_10 -> Any -> Any) -> Any -> T_Fin_10 -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe (T_Fin_10 -> Any -> Any) -> Any -> T_Fin_10 -> Any
du_fold'8242'_298 ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v5 -> (T_Fin_10 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> Any -> Any
v0 Any
v5)) (Any -> Any
forall a b. a -> b
coe Any
v1) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v4))
      T_Fin_10
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.lift
d_lift_318 ::
  Integer ->
  Integer ->
  Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> T_Fin_10
d_lift_318 :: Integer
-> Integer
-> Integer
-> (T_Fin_10 -> T_Fin_10)
-> T_Fin_10
-> T_Fin_10
d_lift_318 ~Integer
v0 ~Integer
v1 Integer
v2 T_Fin_10 -> T_Fin_10
v3 T_Fin_10
v4 = Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> T_Fin_10
du_lift_318 Integer
v2 T_Fin_10 -> T_Fin_10
v3 T_Fin_10
v4
du_lift_318 ::
  Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> T_Fin_10
du_lift_318 :: Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> T_Fin_10
du_lift_318 Integer
v0 T_Fin_10 -> T_Fin_10
v1 T_Fin_10
v2
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
v1 T_Fin_10
v2
      Integer
_ -> let v3 :: Integer
v3 = 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_Fin_10
forall a b. a -> b
coe
             (case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v2 of
                T_Fin_10
C_zero_12 -> T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
C_zero_12
                C_suc_16 T_Fin_10
v5
                  -> (T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16 ((Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> T_Fin_10)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> T_Fin_10
du_lift_318 (Integer -> Any
forall a b. a -> b
coe Integer
v3) ((T_Fin_10 -> T_Fin_10) -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
v1) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v5))
                T_Fin_10
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Fin.Base._+_
d__'43'__338 ::
  Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d__'43'__338 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d__'43'__338 ~Integer
v0 ~Integer
v1 T_Fin_10
v2 T_Fin_10
v3 = T_Fin_10 -> T_Fin_10 -> T_Fin_10
du__'43'__338 T_Fin_10
v2 T_Fin_10
v3
du__'43'__338 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du__'43'__338 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du__'43'__338 T_Fin_10
v0 T_Fin_10
v1
  = case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0 of
      T_Fin_10
C_zero_12 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1
      C_suc_16 T_Fin_10
v3 -> (T_Fin_10 -> T_Fin_10) -> Any -> T_Fin_10
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16 ((T_Fin_10 -> T_Fin_10 -> T_Fin_10) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10 -> T_Fin_10
du__'43'__338 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v3) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v1))
      T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base._-_
d__'45'__350 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d__'45'__350 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d__'45'__350 ~Integer
v0 T_Fin_10
v1 T_Fin_10
v2 = T_Fin_10 -> T_Fin_10 -> T_Fin_10
du__'45'__350 T_Fin_10
v1 T_Fin_10
v2
du__'45'__350 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du__'45'__350 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du__'45'__350 T_Fin_10
v0 T_Fin_10
v1
  = case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
      T_Fin_10
C_zero_12 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0
      C_suc_16 T_Fin_10
v3
        -> case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0 of
             C_suc_16 T_Fin_10
v5 -> (T_Fin_10 -> T_Fin_10 -> T_Fin_10) -> Any -> Any -> T_Fin_10
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10 -> T_Fin_10
du__'45'__350 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v5) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v3)
             T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base._ℕ-_
d__ℕ'45'__362 :: Integer -> T_Fin_10 -> T_Fin_10
d__ℕ'45'__362 :: Integer -> T_Fin_10 -> T_Fin_10
d__ℕ'45'__362 Integer
v0 T_Fin_10
v1
  = case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
      T_Fin_10
C_zero_12 -> (Integer -> T_Fin_10) -> Any -> T_Fin_10
forall a b. a -> b
coe Integer -> T_Fin_10
d_fromℕ_48 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
      C_suc_16 T_Fin_10
v3
        -> 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 -> T_Fin_10
forall a b. a -> b
coe ((Integer -> T_Fin_10 -> T_Fin_10) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_10 -> T_Fin_10
d__ℕ'45'__362 (Integer -> Any
forall a b. a -> b
coe Integer
v4) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v3))
      T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base._ℕ-ℕ_
d__ℕ'45'ℕ__372 :: Integer -> T_Fin_10 -> Integer
d__ℕ'45'ℕ__372 :: Integer -> T_Fin_10 -> Integer
d__ℕ'45'ℕ__372 Integer
v0 T_Fin_10
v1
  = case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
      T_Fin_10
C_zero_12 -> Integer -> Integer
forall a b. a -> b
coe Integer
v0
      C_suc_16 T_Fin_10
v3
        -> 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 -> T_Fin_10 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_10 -> Integer
d__ℕ'45'ℕ__372 (Integer -> Any
forall a b. a -> b
coe Integer
v4) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v3))
      T_Fin_10
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.pred
d_pred_380 :: Integer -> T_Fin_10 -> T_Fin_10
d_pred_380 :: Integer -> T_Fin_10 -> T_Fin_10
d_pred_380 ~Integer
v0 T_Fin_10
v1 = T_Fin_10 -> T_Fin_10
du_pred_380 T_Fin_10
v1
du_pred_380 :: T_Fin_10 -> T_Fin_10
du_pred_380 :: T_Fin_10 -> T_Fin_10
du_pred_380 T_Fin_10
v0
  = case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0 of
      T_Fin_10
C_zero_12 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
C_zero_12
      C_suc_16 T_Fin_10
v2 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v2
      T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.opposite
d_opposite_384 :: Integer -> T_Fin_10 -> T_Fin_10
d_opposite_384 :: Integer -> T_Fin_10 -> T_Fin_10
d_opposite_384 Integer
v0 T_Fin_10
v1
  = 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_Fin_10
forall a b. a -> b
coe
      (case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
         T_Fin_10
C_zero_12 -> (Integer -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_10
d_fromℕ_48 (Integer -> Any
forall a b. a -> b
coe Integer
v2)
         C_suc_16 T_Fin_10
v4 -> (Integer -> T_Fin_10 -> T_Fin_10) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_10 -> T_Fin_10
d_opposite_384 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v4)
         T_Fin_10
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Fin.Base.punchOut
d_punchOut_396 ::
  Integer ->
  T_Fin_10 ->
  T_Fin_10 ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  T_Fin_10
d_punchOut_396 :: Integer
-> T_Fin_10
-> T_Fin_10
-> (T__'8801'__12 -> T_Irrelevant_20)
-> T_Fin_10
d_punchOut_396 ~Integer
v0 T_Fin_10
v1 T_Fin_10
v2 ~T__'8801'__12 -> T_Irrelevant_20
v3 = T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_punchOut_396 T_Fin_10
v1 T_Fin_10
v2
du_punchOut_396 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_punchOut_396 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_punchOut_396 T_Fin_10
v0 T_Fin_10
v1
  = case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0 of
      T_Fin_10
C_zero_12
        -> case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
             T_Fin_10
C_zero_12
               -> ((Any -> T_Irrelevant_20) -> Any) -> Any -> T_Fin_10
forall a b. a -> b
coe
                    (Any -> T_Irrelevant_20) -> Any
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                    Any
forall a. a
erased
             C_suc_16 T_Fin_10
v4 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v4
             T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_suc_16 T_Fin_10
v3
        -> case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
             T_Fin_10
C_zero_12 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
C_zero_12
             C_suc_16 T_Fin_10
v5 -> (T_Fin_10 -> T_Fin_10) -> Any -> T_Fin_10
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16 ((T_Fin_10 -> T_Fin_10 -> T_Fin_10) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_punchOut_396 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v3) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v5))
             T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.punchIn
d_punchIn_410 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_punchIn_410 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_punchIn_410 ~Integer
v0 T_Fin_10
v1 T_Fin_10
v2 = T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_punchIn_410 T_Fin_10
v1 T_Fin_10
v2
du_punchIn_410 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_punchIn_410 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_punchIn_410 T_Fin_10
v0 T_Fin_10
v1
  = case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0 of
      T_Fin_10
C_zero_12 -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16 T_Fin_10
v1
      C_suc_16 T_Fin_10
v3
        -> case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
             T_Fin_10
C_zero_12 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
C_zero_12
             C_suc_16 T_Fin_10
v5 -> (T_Fin_10 -> T_Fin_10) -> Any -> T_Fin_10
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16 ((T_Fin_10 -> T_Fin_10 -> T_Fin_10) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_punchIn_410 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v3) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v5))
             T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.pinch
d_pinch_420 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_pinch_420 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_pinch_420 ~Integer
v0 T_Fin_10
v1 T_Fin_10
v2 = T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_pinch_420 T_Fin_10
v1 T_Fin_10
v2
du_pinch_420 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_pinch_420 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_pinch_420 T_Fin_10
v0 T_Fin_10
v1
  = case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
      T_Fin_10
C_zero_12 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
C_zero_12
      C_suc_16 T_Fin_10
v3
        -> case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0 of
             T_Fin_10
C_zero_12 -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v3
             C_suc_16 T_Fin_10
v5 -> (T_Fin_10 -> T_Fin_10) -> Any -> T_Fin_10
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16 ((T_Fin_10 -> T_Fin_10 -> T_Fin_10) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_pinch_420 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v5) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v3))
             T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Fin_10
_ -> T_Fin_10
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base._≤_
d__'8804'__434 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'8804'__434 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'8804'__434 = Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
forall a. a
erased
-- Data.Fin.Base._≥_
d__'8805'__440 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'8805'__440 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'8805'__440 = Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
forall a. a
erased
-- Data.Fin.Base._<_
d__'60'__446 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'60'__446 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'60'__446 = Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
forall a. a
erased
-- Data.Fin.Base._>_
d__'62'__452 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'62'__452 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'62'__452 = Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
forall a. a
erased
-- Data.Fin.Base._≰_
d__'8816'__460 :: Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'8816'__460 :: Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'8816'__460 = Integer -> T_Fin_10 -> T_Fin_10 -> ()
forall a. a
erased
-- Data.Fin.Base._≮_
d__'8814'__468 :: Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'8814'__468 :: Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'8814'__468 = Integer -> T_Fin_10 -> T_Fin_10 -> ()
forall a. a
erased
-- Data.Fin.Base.Ordering
d_Ordering_476 :: p -> p -> p -> ()
d_Ordering_476 p
a0 p
a1 p
a2 = ()
data T_Ordering_476
  = C_less_484 T_Fin_10 | C_equal_488 | C_greater_494 T_Fin_10
-- Data.Fin.Base.compare
d_compare_500 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Ordering_476
d_compare_500 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Ordering_476
d_compare_500 ~Integer
v0 T_Fin_10
v1 T_Fin_10
v2 = T_Fin_10 -> T_Fin_10 -> T_Ordering_476
du_compare_500 T_Fin_10
v1 T_Fin_10
v2
du_compare_500 :: T_Fin_10 -> T_Fin_10 -> T_Ordering_476
du_compare_500 :: T_Fin_10 -> T_Fin_10 -> T_Ordering_476
du_compare_500 T_Fin_10
v0 T_Fin_10
v1
  = case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0 of
      T_Fin_10
C_zero_12
        -> case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
             T_Fin_10
C_zero_12 -> T_Ordering_476 -> T_Ordering_476
forall a b. a -> b
coe T_Ordering_476
C_equal_488
             C_suc_16 T_Fin_10
v4 -> (T_Fin_10 -> T_Ordering_476) -> Any -> T_Ordering_476
forall a b. a -> b
coe T_Fin_10 -> T_Ordering_476
C_less_484 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
C_zero_12)
             T_Fin_10
_ -> T_Ordering_476
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_suc_16 T_Fin_10
v3
        -> case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
             T_Fin_10
C_zero_12 -> (T_Fin_10 -> T_Ordering_476) -> Any -> T_Ordering_476
forall a b. a -> b
coe T_Fin_10 -> T_Ordering_476
C_greater_494 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
C_zero_12)
             C_suc_16 T_Fin_10
v5
               -> let v6 :: Any
v6 = (T_Fin_10 -> T_Fin_10 -> T_Ordering_476) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10 -> T_Ordering_476
du_compare_500 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v3) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v5) in
                  Any -> T_Ordering_476
forall a b. a -> b
coe
                    (case Any -> T_Ordering_476
forall a b. a -> b
coe Any
v6 of
                       C_less_484 T_Fin_10
v8 -> (T_Fin_10 -> T_Ordering_476) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Ordering_476
C_less_484 ((T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16 T_Fin_10
v8)
                       T_Ordering_476
C_equal_488 -> T_Ordering_476 -> Any
forall a b. a -> b
coe T_Ordering_476
C_equal_488
                       C_greater_494 T_Fin_10
v8 -> (T_Fin_10 -> T_Ordering_476) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Ordering_476
C_greater_494 ((T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
C_suc_16 T_Fin_10
v8)
                       T_Ordering_476
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
             T_Fin_10
_ -> T_Ordering_476
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Fin_10
_ -> T_Ordering_476
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.raise
d_raise_536 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d_raise_536 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d_raise_536 Integer
v0 Integer
v1 T_Fin_10
v2 = (Integer -> T_Fin_10 -> T_Fin_10)
-> Integer -> T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe Integer -> T_Fin_10 -> T_Fin_10
du__'8593''691'__84 Integer
v1 T_Fin_10
v2
-- Data.Fin.Base.inject+
d_inject'43'_542 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d_inject'43'_542 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d_inject'43'_542 ~Integer
v0 ~Integer
v1 T_Fin_10
v2 = T_Fin_10 -> T_Fin_10
du_inject'43'_542 T_Fin_10
v2
du_inject'43'_542 :: T_Fin_10 -> T_Fin_10
du_inject'43'_542 :: T_Fin_10 -> T_Fin_10
du_inject'43'_542 T_Fin_10
v0 = T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0
-- Data.Fin.Base._≺_
d__'8826'__548 :: p -> p -> ()
d__'8826'__548 p
a0 p
a1 = ()
newtype T__'8826'__548 = C__'8827'toℕ__554 T_Fin_10