{-# 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.Data.Empty
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Product
import qualified MAlonzo.Code.Data.Sum.Base

-- Data.Fin.Base.Fin
d_Fin_6 :: p -> ()
d_Fin_6 p
a0 = ()
data T_Fin_6 = C_zero_10 | C_suc_16 T_Fin_6
-- Data.Fin.Base.toℕ
d_toℕ_20 :: Integer -> T_Fin_6 -> Integer
d_toℕ_20 :: Integer -> T_Fin_6 -> Integer
d_toℕ_20 ~Integer
v0 T_Fin_6
v1 = T_Fin_6 -> Integer
du_toℕ_20 T_Fin_6
v1
du_toℕ_20 :: T_Fin_6 -> Integer
du_toℕ_20 :: T_Fin_6 -> Integer
du_toℕ_20 T_Fin_6
v0
  = case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v0 of
      T_Fin_6
C_zero_10 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      C_suc_16 T_Fin_6
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_6 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> Integer
du_toℕ_20 (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v2))
      T_Fin_6
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.Fin′
d_Fin'8242'_26 :: Integer -> T_Fin_6 -> ()
d_Fin'8242'_26 :: Integer -> T_Fin_6 -> ()
d_Fin'8242'_26 = Integer -> T_Fin_6 -> ()
forall a. a
erased
-- Data.Fin.Base.cast
d_cast_36 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T_Fin_6 -> T_Fin_6
d_cast_36 :: Integer -> Integer -> T__'8801'__12 -> T_Fin_6 -> T_Fin_6
d_cast_36 Integer
v0 ~Integer
v1 ~T__'8801'__12
v2 T_Fin_6
v3 = Integer -> T_Fin_6 -> T_Fin_6
du_cast_36 Integer
v0 T_Fin_6
v3
du_cast_36 :: Integer -> T_Fin_6 -> T_Fin_6
du_cast_36 :: Integer -> T_Fin_6 -> T_Fin_6
du_cast_36 Integer
v0 T_Fin_6
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1
      Integer
_ -> case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1 of
             T_Fin_6
C_zero_10 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
C_zero_10
             C_suc_16 T_Fin_6
v3
               -> (T_Fin_6 -> T_Fin_6) -> Any -> T_Fin_6
forall a b. a -> b
coe
                    T_Fin_6 -> T_Fin_6
C_suc_16
                    ((Integer -> T_Fin_6 -> T_Fin_6) -> Any -> Any -> Any
forall a b. a -> b
coe
                       Integer -> T_Fin_6 -> T_Fin_6
du_cast_36
                       ((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_6 -> Any
forall a b. a -> b
coe T_Fin_6
v3))
             T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.fromℕ
d_fromℕ_58 :: Integer -> T_Fin_6
d_fromℕ_58 :: Integer -> T_Fin_6
d_fromℕ_58 Integer
v0
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
C_zero_10
      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_6
forall a b. a -> b
coe ((T_Fin_6 -> T_Fin_6) -> T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
C_suc_16 (Integer -> T_Fin_6
d_fromℕ_58 (Integer -> Integer
forall a b. a -> b
coe Integer
v1)))
-- Data.Fin.Base.fromℕ<
d_fromℕ'60'_66 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__18 -> T_Fin_6
d_fromℕ'60'_66 :: Integer -> Integer -> T__'8804'__18 -> T_Fin_6
d_fromℕ'60'_66 Integer
v0 ~Integer
v1 ~T__'8804'__18
v2 = Integer -> T_Fin_6
du_fromℕ'60'_66 Integer
v0
du_fromℕ'60'_66 :: Integer -> T_Fin_6
du_fromℕ'60'_66 :: Integer -> T_Fin_6
du_fromℕ'60'_66 Integer
v0
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
C_zero_10
      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_6
forall a b. a -> b
coe ((T_Fin_6 -> T_Fin_6) -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
C_suc_16 ((Integer -> T_Fin_6) -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_6
du_fromℕ'60'_66 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
-- Data.Fin.Base.fromℕ<″
d_fromℕ'60''8243'_82 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804''8243'__188 -> T_Fin_6
d_fromℕ'60''8243'_82 :: Integer -> Integer -> T__'8804''8243'__188 -> T_Fin_6
d_fromℕ'60''8243'_82 Integer
v0 ~Integer
v1 T__'8804''8243'__188
v2 = Integer -> T__'8804''8243'__188 -> T_Fin_6
du_fromℕ'60''8243'_82 Integer
v0 T__'8804''8243'__188
v2
du_fromℕ'60''8243'_82 ::
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804''8243'__188 -> T_Fin_6
du_fromℕ'60''8243'_82 :: Integer -> T__'8804''8243'__188 -> T_Fin_6
du_fromℕ'60''8243'_82 Integer
v0 T__'8804''8243'__188
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> (Any -> Any -> Any) -> Any -> Any -> T_Fin_6
forall a b. a -> b
coe Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'8804''8243'__188 -> Any
forall a b. a -> b
coe T__'8804''8243'__188
v1) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
C_zero_10)
      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_6
forall a b. a -> b
coe
             (case T__'8804''8243'__188 -> T__'8804''8243'__188
forall a b. a -> b
coe T__'8804''8243'__188
v1 of
                MAlonzo.Code.Data.Nat.Base.C_less'45'than'45'or'45'equal_202 Integer
v3
                  -> (T_Fin_6 -> T_Fin_6) -> Any -> Any
forall a b. a -> b
coe
                       T_Fin_6 -> T_Fin_6
C_suc_16
                       ((Integer -> T__'8804''8243'__188 -> T_Fin_6) -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> T__'8804''8243'__188 -> T_Fin_6
du_fromℕ'60''8243'_82 (Integer -> Any
forall a b. a -> b
coe Integer
v2)
                          ((Integer -> T__'8804''8243'__188) -> Integer -> Any
forall a b. a -> b
coe
                             Integer -> T__'8804''8243'__188
MAlonzo.Code.Data.Nat.Base.C_less'45'than'45'or'45'equal_202 Integer
v3))
                T__'8804''8243'__188
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Fin.Base.raise
d_raise_90 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6
d_raise_90 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6
d_raise_90 ~Integer
v0 Integer
v1 T_Fin_6
v2 = Integer -> T_Fin_6 -> T_Fin_6
du_raise_90 Integer
v1 T_Fin_6
v2
du_raise_90 :: Integer -> T_Fin_6 -> T_Fin_6
du_raise_90 :: Integer -> T_Fin_6 -> T_Fin_6
du_raise_90 Integer
v0 T_Fin_6
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
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_6
forall a b. a -> b
coe ((T_Fin_6 -> T_Fin_6) -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
C_suc_16 ((Integer -> T_Fin_6 -> T_Fin_6) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_6 -> T_Fin_6
du_raise_90 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v1)))
-- Data.Fin.Base.reduce≥
d_reduce'8805'_106 ::
  Integer ->
  Integer ->
  T_Fin_6 -> MAlonzo.Code.Data.Nat.Base.T__'8804'__18 -> T_Fin_6
d_reduce'8805'_106 :: Integer -> Integer -> T_Fin_6 -> T__'8804'__18 -> T_Fin_6
d_reduce'8805'_106 Integer
v0 ~Integer
v1 T_Fin_6
v2 T__'8804'__18
v3 = Integer -> T_Fin_6 -> T__'8804'__18 -> T_Fin_6
du_reduce'8805'_106 Integer
v0 T_Fin_6
v2 T__'8804'__18
v3
du_reduce'8805'_106 ::
  Integer ->
  T_Fin_6 -> MAlonzo.Code.Data.Nat.Base.T__'8804'__18 -> T_Fin_6
du_reduce'8805'_106 :: Integer -> T_Fin_6 -> T__'8804'__18 -> T_Fin_6
du_reduce'8805'_106 Integer
v0 T_Fin_6
v1 T__'8804'__18
v2
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1
      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_6
forall a b. a -> b
coe
             (case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1 of
                C_suc_16 T_Fin_6
v5
                  -> case T__'8804'__18 -> T__'8804'__18
forall a b. a -> b
coe T__'8804'__18
v2 of
                       MAlonzo.Code.Data.Nat.Base.C_s'8804's_30 T__'8804'__18
v8
                         -> (Integer -> T_Fin_6 -> T__'8804'__18 -> T_Fin_6)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_6 -> T__'8804'__18 -> T_Fin_6
du_reduce'8805'_106 (Integer -> Any
forall a b. a -> b
coe Integer
v3) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v5) (T__'8804'__18 -> Any
forall a b. a -> b
coe T__'8804'__18
v8)
                       T__'8804'__18
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                T_Fin_6
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Fin.Base.inject
d_inject_122 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
d_inject_122 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
d_inject_122 ~Integer
v0 T_Fin_6
v1 T_Fin_6
v2 = T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_inject_122 T_Fin_6
v1 T_Fin_6
v2
du_inject_122 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_inject_122 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_inject_122 T_Fin_6
v0 T_Fin_6
v1
  = case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v0 of
      C_suc_16 T_Fin_6
v3
        -> case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1 of
             T_Fin_6
C_zero_10 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
C_zero_10
             C_suc_16 T_Fin_6
v5 -> (T_Fin_6 -> T_Fin_6) -> Any -> T_Fin_6
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
C_suc_16 ((T_Fin_6 -> T_Fin_6 -> T_Fin_6) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_inject_122 (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v3) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v5))
             T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.inject!
d_inject'33'_134 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
d_inject'33'_134 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
d_inject'33'_134 ~Integer
v0 T_Fin_6
v1 T_Fin_6
v2 = T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_inject'33'_134 T_Fin_6
v1 T_Fin_6
v2
du_inject'33'_134 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_inject'33'_134 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_inject'33'_134 T_Fin_6
v0 T_Fin_6
v1
  = case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v0 of
      C_suc_16 T_Fin_6
v3
        -> case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1 of
             T_Fin_6
C_zero_10 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
C_zero_10
             C_suc_16 T_Fin_6
v5
               -> (T_Fin_6 -> T_Fin_6) -> Any -> T_Fin_6
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
C_suc_16 ((T_Fin_6 -> T_Fin_6 -> T_Fin_6) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_inject'33'_134 (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v3) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v5))
             T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.inject+
d_inject'43'_142 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6
d_inject'43'_142 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6
d_inject'43'_142 ~Integer
v0 ~Integer
v1 T_Fin_6
v2 = T_Fin_6 -> T_Fin_6
du_inject'43'_142 T_Fin_6
v2
du_inject'43'_142 :: T_Fin_6 -> T_Fin_6
du_inject'43'_142 :: T_Fin_6 -> T_Fin_6
du_inject'43'_142 T_Fin_6
v0 = T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v0
-- Data.Fin.Base.inject₁
d_inject'8321'_152 :: Integer -> T_Fin_6 -> T_Fin_6
d_inject'8321'_152 :: Integer -> T_Fin_6 -> T_Fin_6
d_inject'8321'_152 ~Integer
v0 T_Fin_6
v1 = T_Fin_6 -> T_Fin_6
du_inject'8321'_152 T_Fin_6
v1
du_inject'8321'_152 :: T_Fin_6 -> T_Fin_6
du_inject'8321'_152 :: T_Fin_6 -> T_Fin_6
du_inject'8321'_152 T_Fin_6
v0 = T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v0
-- Data.Fin.Base.inject≤
d_inject'8804'_160 ::
  Integer ->
  Integer ->
  T_Fin_6 -> MAlonzo.Code.Data.Nat.Base.T__'8804'__18 -> T_Fin_6
d_inject'8804'_160 :: Integer -> Integer -> T_Fin_6 -> T__'8804'__18 -> T_Fin_6
d_inject'8804'_160 ~Integer
v0 ~Integer
v1 T_Fin_6
v2 ~T__'8804'__18
v3 = T_Fin_6 -> T_Fin_6
du_inject'8804'_160 T_Fin_6
v2
du_inject'8804'_160 :: T_Fin_6 -> T_Fin_6
du_inject'8804'_160 :: T_Fin_6 -> T_Fin_6
du_inject'8804'_160 T_Fin_6
v0 = T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v0
-- Data.Fin.Base.lower₁
d_lower'8321'_176 ::
  Integer ->
  T_Fin_6 ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  T_Fin_6
d_lower'8321'_176 :: Integer -> T_Fin_6 -> (T__'8801'__12 -> T_'8869'_4) -> T_Fin_6
d_lower'8321'_176 Integer
v0 T_Fin_6
v1 ~T__'8801'__12 -> T_'8869'_4
v2 = Integer -> T_Fin_6 -> T_Fin_6
du_lower'8321'_176 Integer
v0 T_Fin_6
v1
du_lower'8321'_176 :: Integer -> T_Fin_6 -> T_Fin_6
du_lower'8321'_176 :: Integer -> T_Fin_6 -> T_Fin_6
du_lower'8321'_176 Integer
v0 T_Fin_6
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> (Any -> Any -> Any) -> Any -> Any -> T_Fin_6
forall a b. a -> b
coe
             Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v1) (Any -> Any
forall a b. a -> b
coe Any
MAlonzo.Code.Data.Empty.du_'8869''45'elim_10)
      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_6
forall a b. a -> b
coe
             (case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1 of
                T_Fin_6
C_zero_10 -> T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
C_zero_10
                C_suc_16 T_Fin_6
v4
                  -> (T_Fin_6 -> T_Fin_6) -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
C_suc_16 ((Integer -> T_Fin_6 -> T_Fin_6) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_6 -> T_Fin_6
du_lower'8321'_176 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v4))
                T_Fin_6
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Fin.Base.strengthen
d_strengthen_194 :: Integer -> T_Fin_6 -> T_Fin_6
d_strengthen_194 :: Integer -> T_Fin_6 -> T_Fin_6
d_strengthen_194 ~Integer
v0 T_Fin_6
v1 = T_Fin_6 -> T_Fin_6
du_strengthen_194 T_Fin_6
v1
du_strengthen_194 :: T_Fin_6 -> T_Fin_6
du_strengthen_194 :: T_Fin_6 -> T_Fin_6
du_strengthen_194 T_Fin_6
v0 = T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v0
-- Data.Fin.Base.splitAt
d_splitAt_202 ::
  Integer ->
  Integer -> T_Fin_6 -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_splitAt_202 :: Integer -> Integer -> T_Fin_6 -> T__'8846'__30
d_splitAt_202 Integer
v0 ~Integer
v1 T_Fin_6
v2 = Integer -> T_Fin_6 -> T__'8846'__30
du_splitAt_202 Integer
v0 T_Fin_6
v2
du_splitAt_202 ::
  Integer -> T_Fin_6 -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_splitAt_202 :: Integer -> T_Fin_6 -> T__'8846'__30
du_splitAt_202 Integer
v0 T_Fin_6
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_6 -> Any
forall a b. a -> b
coe T_Fin_6
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_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1 of
                T_Fin_6
C_zero_10
                  -> (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_6 -> Any
forall a b. a -> b
coe T_Fin_6
C_zero_10)
                C_suc_16 T_Fin_6
v4
                  -> ((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30)
-> Any -> (Any -> Any) -> Any -> Any
forall a b. a -> b
coe
                       (Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84 ((T_Fin_6 -> T_Fin_6) -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
C_suc_16) (\ Any
v5 -> Any
v5)
                       ((Integer -> T_Fin_6 -> T__'8846'__30) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_6 -> T__'8846'__30
du_splitAt_202 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v4))
                T_Fin_6
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Fin.Base.join
d_join_216 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Fin_6
d_join_216 :: Integer -> Integer -> T__'8846'__30 -> T_Fin_6
d_join_216 Integer
v0 ~Integer
v1 = Integer -> T__'8846'__30 -> T_Fin_6
du_join_216 Integer
v0
du_join_216 ::
  Integer -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Fin_6
du_join_216 :: Integer -> T__'8846'__30 -> T_Fin_6
du_join_216 Integer
v0
  = ((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> Any)
-> (Any -> Any) -> Any -> T__'8846'__30 -> T_Fin_6
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_6 -> T_Fin_6) -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_6 -> T_Fin_6
du_raise_90 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
-- Data.Fin.Base.quotRem
d_quotRem_226 ::
  Integer ->
  Integer -> T_Fin_6 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_quotRem_226 :: Integer -> Integer -> T_Fin_6 -> T_Σ_14
d_quotRem_226 ~Integer
v0 Integer
v1 T_Fin_6
v2 = Integer -> T_Fin_6 -> T_Σ_14
du_quotRem_226 Integer
v1 T_Fin_6
v2
du_quotRem_226 ::
  Integer -> T_Fin_6 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_quotRem_226 :: Integer -> T_Fin_6 -> T_Σ_14
du_quotRem_226 Integer
v0 T_Fin_6
v1
  = let v2 :: t
v2 = (Integer -> T_Fin_6 -> T__'8846'__30) -> Any -> Any -> t
forall a b. a -> b
coe Integer -> T_Fin_6 -> T__'8846'__30
du_splitAt_202 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v1) in
    Any -> T_Σ_14
forall a b. a -> b
coe
      (case Any -> T__'8846'__30
forall a b. a -> b
coe Any
forall a. a
v2 of
         MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
v3
           -> (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
v3)
                (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
C_zero_10)
         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
v3
           -> ((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.du_map'8322'_170 (\ Any
v4 -> (T_Fin_6 -> T_Fin_6) -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
C_suc_16)
                ((Integer -> T_Fin_6 -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_6 -> T_Σ_14
du_quotRem_226 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Any -> Any
forall a b. a -> b
coe Any
v3))
         T__'8846'__30
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Fin.Base.remQuot
d_remQuot_258 ::
  Integer ->
  Integer -> T_Fin_6 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_remQuot_258 :: Integer -> Integer -> T_Fin_6 -> T_Σ_14
d_remQuot_258 ~Integer
v0 Integer
v1 T_Fin_6
v2 = Integer -> T_Fin_6 -> T_Σ_14
du_remQuot_258 Integer
v1 T_Fin_6
v2
du_remQuot_258 ::
  Integer -> T_Fin_6 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_remQuot_258 :: Integer -> T_Fin_6 -> T_Σ_14
du_remQuot_258 Integer
v0 T_Fin_6
v1
  = (T_Σ_14 -> T_Σ_14) -> Any -> T_Σ_14
forall a b. a -> b
coe
      T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_swap_386
      ((Integer -> T_Fin_6 -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_6 -> T_Σ_14
du_quotRem_226 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v1))
-- Data.Fin.Base.combine
d_combine_266 ::
  Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
d_combine_266 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
d_combine_266 ~Integer
v0 Integer
v1 T_Fin_6
v2 T_Fin_6
v3 = Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_combine_266 Integer
v1 T_Fin_6
v2 T_Fin_6
v3
du_combine_266 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_combine_266 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_combine_266 Integer
v0 T_Fin_6
v1 T_Fin_6
v2
  = case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1 of
      T_Fin_6
C_zero_10 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v2
      C_suc_16 T_Fin_6
v4
        -> (Integer -> T_Fin_6 -> T_Fin_6) -> Any -> Any -> T_Fin_6
forall a b. a -> b
coe
             Integer -> T_Fin_6 -> T_Fin_6
du_raise_90 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
             ((Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_combine_266 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v4) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v2))
      T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.fold
d_fold_292 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (Integer -> ()) ->
  Integer ->
  (Integer -> AgdaAny -> AgdaAny) ->
  (Integer -> AgdaAny) -> T_Fin_6 -> AgdaAny
d_fold_292 :: ()
-> (Integer -> ())
-> Integer
-> (Integer -> Any -> Any)
-> (Integer -> Any)
-> T_Fin_6
-> Any
d_fold_292 ~()
v0 ~Integer -> ()
v1 Integer
v2 Integer -> Any -> Any
v3 Integer -> Any
v4 T_Fin_6
v5 = Integer
-> (Integer -> Any -> Any) -> (Integer -> Any) -> T_Fin_6 -> Any
du_fold_292 Integer
v2 Integer -> Any -> Any
v3 Integer -> Any
v4 T_Fin_6
v5
du_fold_292 ::
  Integer ->
  (Integer -> AgdaAny -> AgdaAny) ->
  (Integer -> AgdaAny) -> T_Fin_6 -> AgdaAny
du_fold_292 :: Integer
-> (Integer -> Any -> Any) -> (Integer -> Any) -> T_Fin_6 -> Any
du_fold_292 Integer
v0 Integer -> Any -> Any
v1 Integer -> Any
v2 T_Fin_6
v3
  = case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v3 of
      T_Fin_6
C_zero_10
        -> 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_6
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_6 -> Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer
-> (Integer -> Any -> Any) -> (Integer -> Any) -> T_Fin_6 -> Any
du_fold_292 (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_6 -> Any
forall a b. a -> b
coe T_Fin_6
v5)))
      T_Fin_6
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.fold′
d_fold'8242'_318 ::
  Integer ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (T_Fin_6 -> ()) ->
  (T_Fin_6 -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Fin_6 -> AgdaAny
d_fold'8242'_318 :: Integer
-> ()
-> (T_Fin_6 -> ())
-> (T_Fin_6 -> Any -> Any)
-> Any
-> T_Fin_6
-> Any
d_fold'8242'_318 ~Integer
v0 ~()
v1 ~T_Fin_6 -> ()
v2 T_Fin_6 -> Any -> Any
v3 Any
v4 T_Fin_6
v5 = (T_Fin_6 -> Any -> Any) -> Any -> T_Fin_6 -> Any
du_fold'8242'_318 T_Fin_6 -> Any -> Any
v3 Any
v4 T_Fin_6
v5
du_fold'8242'_318 ::
  (T_Fin_6 -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Fin_6 -> AgdaAny
du_fold'8242'_318 :: (T_Fin_6 -> Any -> Any) -> Any -> T_Fin_6 -> Any
du_fold'8242'_318 T_Fin_6 -> Any -> Any
v0 Any
v1 T_Fin_6
v2
  = case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v2 of
      T_Fin_6
C_zero_10 -> Any -> Any
forall a b. a -> b
coe Any
v1
      C_suc_16 T_Fin_6
v4
        -> (T_Fin_6 -> Any -> Any) -> T_Fin_6 -> Any -> Any
forall a b. a -> b
coe
             T_Fin_6 -> Any -> Any
v0 T_Fin_6
v4
             (((T_Fin_6 -> Any -> Any) -> Any -> T_Fin_6 -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe (T_Fin_6 -> Any -> Any) -> Any -> T_Fin_6 -> Any
du_fold'8242'_318 ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v5 -> (T_Fin_6 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> Any -> Any
v0 Any
v5)) (Any -> Any
forall a b. a -> b
coe Any
v1) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v4))
      T_Fin_6
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.lift
d_lift_342 ::
  Integer ->
  Integer -> Integer -> (T_Fin_6 -> T_Fin_6) -> T_Fin_6 -> T_Fin_6
d_lift_342 :: Integer
-> Integer -> Integer -> (T_Fin_6 -> T_Fin_6) -> T_Fin_6 -> T_Fin_6
d_lift_342 ~Integer
v0 ~Integer
v1 Integer
v2 T_Fin_6 -> T_Fin_6
v3 T_Fin_6
v4 = Integer -> (T_Fin_6 -> T_Fin_6) -> T_Fin_6 -> T_Fin_6
du_lift_342 Integer
v2 T_Fin_6 -> T_Fin_6
v3 T_Fin_6
v4
du_lift_342 ::
  Integer -> (T_Fin_6 -> T_Fin_6) -> T_Fin_6 -> T_Fin_6
du_lift_342 :: Integer -> (T_Fin_6 -> T_Fin_6) -> T_Fin_6 -> T_Fin_6
du_lift_342 Integer
v0 T_Fin_6 -> T_Fin_6
v1 T_Fin_6
v2
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> (T_Fin_6 -> T_Fin_6) -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
v1 T_Fin_6
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_6
forall a b. a -> b
coe
             (case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v2 of
                T_Fin_6
C_zero_10 -> T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
C_zero_10
                C_suc_16 T_Fin_6
v5
                  -> (T_Fin_6 -> T_Fin_6) -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
C_suc_16 ((Integer -> (T_Fin_6 -> T_Fin_6) -> T_Fin_6 -> T_Fin_6)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> (T_Fin_6 -> T_Fin_6) -> T_Fin_6 -> T_Fin_6
du_lift_342 (Integer -> Any
forall a b. a -> b
coe Integer
v3) ((T_Fin_6 -> T_Fin_6) -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
v1) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v5))
                T_Fin_6
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Fin.Base._+_
d__'43'__366 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
d__'43'__366 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
d__'43'__366 ~Integer
v0 ~Integer
v1 T_Fin_6
v2 T_Fin_6
v3 = T_Fin_6 -> T_Fin_6 -> T_Fin_6
du__'43'__366 T_Fin_6
v2 T_Fin_6
v3
du__'43'__366 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6
du__'43'__366 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6
du__'43'__366 T_Fin_6
v0 T_Fin_6
v1
  = case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v0 of
      T_Fin_6
C_zero_10 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1
      C_suc_16 T_Fin_6
v3 -> (T_Fin_6 -> T_Fin_6) -> Any -> T_Fin_6
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
C_suc_16 ((T_Fin_6 -> T_Fin_6 -> T_Fin_6) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6 -> T_Fin_6
du__'43'__366 (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v3) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v1))
      T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base._-_
d__'45'__380 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
d__'45'__380 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
d__'45'__380 ~Integer
v0 T_Fin_6
v1 T_Fin_6
v2 = T_Fin_6 -> T_Fin_6 -> T_Fin_6
du__'45'__380 T_Fin_6
v1 T_Fin_6
v2
du__'45'__380 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6
du__'45'__380 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6
du__'45'__380 T_Fin_6
v0 T_Fin_6
v1
  = case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1 of
      T_Fin_6
C_zero_10 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v0
      C_suc_16 T_Fin_6
v3
        -> case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v0 of
             C_suc_16 T_Fin_6
v5 -> (T_Fin_6 -> T_Fin_6 -> T_Fin_6) -> Any -> Any -> T_Fin_6
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6 -> T_Fin_6
du__'45'__380 (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v5) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v3)
             T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base._ℕ-_
d__ℕ'45'__392 :: Integer -> T_Fin_6 -> T_Fin_6
d__ℕ'45'__392 :: Integer -> T_Fin_6 -> T_Fin_6
d__ℕ'45'__392 Integer
v0 T_Fin_6
v1
  = case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1 of
      T_Fin_6
C_zero_10 -> (Integer -> T_Fin_6) -> Any -> T_Fin_6
forall a b. a -> b
coe Integer -> T_Fin_6
d_fromℕ_58 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
      C_suc_16 T_Fin_6
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_6
forall a b. a -> b
coe ((Integer -> T_Fin_6 -> T_Fin_6) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_6 -> T_Fin_6
d__ℕ'45'__392 (Integer -> Any
forall a b. a -> b
coe Integer
v4) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v3))
      T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base._ℕ-ℕ_
d__ℕ'45'ℕ__402 :: Integer -> T_Fin_6 -> Integer
d__ℕ'45'ℕ__402 :: Integer -> T_Fin_6 -> Integer
d__ℕ'45'ℕ__402 Integer
v0 T_Fin_6
v1
  = case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1 of
      T_Fin_6
C_zero_10 -> Integer -> Integer
forall a b. a -> b
coe Integer
v0
      C_suc_16 T_Fin_6
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_6 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_6 -> Integer
d__ℕ'45'ℕ__402 (Integer -> Any
forall a b. a -> b
coe Integer
v4) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v3))
      T_Fin_6
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.pred
d_pred_412 :: Integer -> T_Fin_6 -> T_Fin_6
d_pred_412 :: Integer -> T_Fin_6 -> T_Fin_6
d_pred_412 ~Integer
v0 T_Fin_6
v1 = T_Fin_6 -> T_Fin_6
du_pred_412 T_Fin_6
v1
du_pred_412 :: T_Fin_6 -> T_Fin_6
du_pred_412 :: T_Fin_6 -> T_Fin_6
du_pred_412 T_Fin_6
v0
  = case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v0 of
      T_Fin_6
C_zero_10 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
C_zero_10
      C_suc_16 T_Fin_6
v2 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v2
      T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.opposite
d_opposite_418 :: Integer -> T_Fin_6 -> T_Fin_6
d_opposite_418 :: Integer -> T_Fin_6 -> T_Fin_6
d_opposite_418 Integer
v0 T_Fin_6
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_6
forall a b. a -> b
coe
      (case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1 of
         T_Fin_6
C_zero_10 -> (Integer -> T_Fin_6) -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_6
d_fromℕ_58 (Integer -> Any
forall a b. a -> b
coe Integer
v2)
         C_suc_16 T_Fin_6
v4 -> (Integer -> T_Fin_6 -> T_Fin_6) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Fin_6 -> T_Fin_6
d_opposite_418 (Integer -> Any
forall a b. a -> b
coe Integer
v2) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v4)
         T_Fin_6
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Fin.Base.punchOut
d_punchOut_432 ::
  Integer ->
  T_Fin_6 ->
  T_Fin_6 ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  T_Fin_6
d_punchOut_432 :: Integer
-> T_Fin_6 -> T_Fin_6 -> (T__'8801'__12 -> T_'8869'_4) -> T_Fin_6
d_punchOut_432 ~Integer
v0 T_Fin_6
v1 T_Fin_6
v2 ~T__'8801'__12 -> T_'8869'_4
v3 = T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_punchOut_432 T_Fin_6
v1 T_Fin_6
v2
du_punchOut_432 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_punchOut_432 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_punchOut_432 T_Fin_6
v0 T_Fin_6
v1
  = case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v0 of
      T_Fin_6
C_zero_10
        -> case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1 of
             T_Fin_6
C_zero_10 -> Any -> T_Fin_6
forall a b. a -> b
coe Any
MAlonzo.Code.Data.Empty.du_'8869''45'elim_10
             C_suc_16 T_Fin_6
v4 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v4
             T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_suc_16 T_Fin_6
v3
        -> case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1 of
             T_Fin_6
C_zero_10 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
C_zero_10
             C_suc_16 T_Fin_6
v5 -> (T_Fin_6 -> T_Fin_6) -> Any -> T_Fin_6
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
C_suc_16 ((T_Fin_6 -> T_Fin_6 -> T_Fin_6) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_punchOut_432 (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v3) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v5))
             T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.punchIn
d_punchIn_452 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
d_punchIn_452 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
d_punchIn_452 ~Integer
v0 T_Fin_6
v1 T_Fin_6
v2 = T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_punchIn_452 T_Fin_6
v1 T_Fin_6
v2
du_punchIn_452 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_punchIn_452 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_punchIn_452 T_Fin_6
v0 T_Fin_6
v1
  = case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v0 of
      T_Fin_6
C_zero_10 -> (T_Fin_6 -> T_Fin_6) -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
C_suc_16 T_Fin_6
v1
      C_suc_16 T_Fin_6
v3
        -> case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1 of
             T_Fin_6
C_zero_10 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
C_zero_10
             C_suc_16 T_Fin_6
v5 -> (T_Fin_6 -> T_Fin_6) -> Any -> T_Fin_6
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
C_suc_16 ((T_Fin_6 -> T_Fin_6 -> T_Fin_6) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_punchIn_452 (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v3) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v5))
             T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.pinch
d_pinch_464 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
d_pinch_464 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6
d_pinch_464 ~Integer
v0 T_Fin_6
v1 T_Fin_6
v2 = T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_pinch_464 T_Fin_6
v1 T_Fin_6
v2
du_pinch_464 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_pinch_464 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_pinch_464 T_Fin_6
v0 T_Fin_6
v1
  = case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1 of
      T_Fin_6
C_zero_10 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
C_zero_10
      C_suc_16 T_Fin_6
v3
        -> case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v0 of
             T_Fin_6
C_zero_10 -> T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v3
             C_suc_16 T_Fin_6
v5 -> (T_Fin_6 -> T_Fin_6) -> Any -> T_Fin_6
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
C_suc_16 ((T_Fin_6 -> T_Fin_6 -> T_Fin_6) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6 -> T_Fin_6
du_pinch_464 (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v5) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v3))
             T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Fin_6
_ -> T_Fin_6
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base._≤_
d__'8804'__480 :: Integer -> T_Fin_6 -> T_Fin_6 -> ()
d__'8804'__480 :: Integer -> T_Fin_6 -> T_Fin_6 -> ()
d__'8804'__480 = Integer -> T_Fin_6 -> T_Fin_6 -> ()
forall a. a
erased
-- Data.Fin.Base._≥_
d__'8805'__484 :: Integer -> T_Fin_6 -> T_Fin_6 -> ()
d__'8805'__484 :: Integer -> T_Fin_6 -> T_Fin_6 -> ()
d__'8805'__484 = Integer -> T_Fin_6 -> T_Fin_6 -> ()
forall a. a
erased
-- Data.Fin.Base._<_
d__'60'__488 :: Integer -> T_Fin_6 -> T_Fin_6 -> ()
d__'60'__488 :: Integer -> T_Fin_6 -> T_Fin_6 -> ()
d__'60'__488 = Integer -> T_Fin_6 -> T_Fin_6 -> ()
forall a. a
erased
-- Data.Fin.Base._>_
d__'62'__492 :: Integer -> T_Fin_6 -> T_Fin_6 -> ()
d__'62'__492 :: Integer -> T_Fin_6 -> T_Fin_6 -> ()
d__'62'__492 = Integer -> T_Fin_6 -> T_Fin_6 -> ()
forall a. a
erased
-- Data.Fin.Base._≺_
d__'8826'__494 :: p -> p -> ()
d__'8826'__494 p
a0 p
a1 = ()
newtype T__'8826'__494 = C__'8827'toℕ__500 T_Fin_6
-- Data.Fin.Base.Ordering
d_Ordering_504 :: p -> p -> p -> ()
d_Ordering_504 p
a0 p
a1 p
a2 = ()
data T_Ordering_504
  = C_less_512 T_Fin_6 | C_equal_516 | C_greater_522 T_Fin_6
-- Data.Fin.Base.compare
d_compare_530 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Ordering_504
d_compare_530 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Ordering_504
d_compare_530 ~Integer
v0 T_Fin_6
v1 T_Fin_6
v2 = T_Fin_6 -> T_Fin_6 -> T_Ordering_504
du_compare_530 T_Fin_6
v1 T_Fin_6
v2
du_compare_530 :: T_Fin_6 -> T_Fin_6 -> T_Ordering_504
du_compare_530 :: T_Fin_6 -> T_Fin_6 -> T_Ordering_504
du_compare_530 T_Fin_6
v0 T_Fin_6
v1
  = case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v0 of
      T_Fin_6
C_zero_10
        -> case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1 of
             T_Fin_6
C_zero_10 -> T_Ordering_504 -> T_Ordering_504
forall a b. a -> b
coe T_Ordering_504
C_equal_516
             C_suc_16 T_Fin_6
v4 -> (T_Fin_6 -> T_Ordering_504) -> Any -> T_Ordering_504
forall a b. a -> b
coe T_Fin_6 -> T_Ordering_504
C_less_512 (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
C_zero_10)
             T_Fin_6
_ -> T_Ordering_504
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_suc_16 T_Fin_6
v3
        -> case T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
v1 of
             T_Fin_6
C_zero_10 -> (T_Fin_6 -> T_Ordering_504) -> Any -> T_Ordering_504
forall a b. a -> b
coe T_Fin_6 -> T_Ordering_504
C_greater_522 (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
C_zero_10)
             C_suc_16 T_Fin_6
v5
               -> let v6 :: t
v6 = (T_Fin_6 -> T_Fin_6 -> T_Ordering_504) -> Any -> Any -> t
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6 -> T_Ordering_504
du_compare_530 (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v3) (T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6
v5) in
                  Any -> T_Ordering_504
forall a b. a -> b
coe
                    (case Any -> T_Ordering_504
forall a b. a -> b
coe Any
forall a. a
v6 of
                       C_less_512 T_Fin_6
v8 -> (T_Fin_6 -> T_Ordering_504) -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Ordering_504
C_less_512 ((T_Fin_6 -> T_Fin_6) -> T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
C_suc_16 T_Fin_6
v8)
                       T_Ordering_504
C_equal_516 -> T_Ordering_504 -> Any
forall a b. a -> b
coe T_Ordering_504
C_equal_516
                       C_greater_522 T_Fin_6
v8 -> (T_Fin_6 -> T_Ordering_504) -> Any -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Ordering_504
C_greater_522 ((T_Fin_6 -> T_Fin_6) -> T_Fin_6 -> Any
forall a b. a -> b
coe T_Fin_6 -> T_Fin_6
C_suc_16 T_Fin_6
v8)
                       T_Ordering_504
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
             T_Fin_6
_ -> T_Ordering_504
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Fin_6
_ -> T_Ordering_504
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Fin.Base.fromℕ≤
d_fromℕ'8804'_566 ::
  Integer ->
  Integer -> MAlonzo.Code.Data.Nat.Base.T__'8804'__18 -> T_Fin_6
d_fromℕ'8804'_566 :: Integer -> Integer -> T__'8804'__18 -> T_Fin_6
d_fromℕ'8804'_566 Integer
v0 Integer
v1 T__'8804'__18
v2 = (Integer -> T_Fin_6) -> Integer -> T_Fin_6
forall a b. a -> b
coe Integer -> T_Fin_6
du_fromℕ'60'_66 Integer
v0
-- Data.Fin.Base.fromℕ≤″
d_fromℕ'8804''8243'_568 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Nat.Base.T__'8804''8243'__188 -> T_Fin_6
d_fromℕ'8804''8243'_568 :: Integer -> Integer -> T__'8804''8243'__188 -> T_Fin_6
d_fromℕ'8804''8243'_568 Integer
v0 Integer
v1 T__'8804''8243'__188
v2 = (Integer -> T__'8804''8243'__188 -> T_Fin_6)
-> Integer -> T__'8804''8243'__188 -> T_Fin_6
forall a b. a -> b
coe Integer -> T__'8804''8243'__188 -> T_Fin_6
du_fromℕ'60''8243'_82 Integer
v0 T__'8804''8243'__188
v2