{-# 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
d_Fin_6 :: p -> ()
d_Fin_6 p
a0 = ()
data T_Fin_6 = C_zero_10 | C_suc_16 T_Fin_6
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
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
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
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)))
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)))
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)
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)))
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)
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
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
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
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
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
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)
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
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)
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))
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)
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))
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
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
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
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)
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
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
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
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
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
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)
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
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
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
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
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
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
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
d__'8826'__494 :: p -> p -> ()
d__'8826'__494 p
a0 p
a1 = ()
newtype T__'8826'__494 = C__'8827'toℕ__500 T_Fin_6
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
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
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
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