{-# 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
d_Fin_10 :: p -> ()
d_Fin_10 p
a0 = ()
data T_Fin_10 = C_zero_12 | C_suc_16 T_Fin_10
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
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
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
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)))
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)))
d_fromℕ'60''8243'_62 ::
Integer ->
Integer ->
MAlonzo.Code.Algebra.Definitions.RawMagma.T__'8739''737'__26 ->
T_Fin_10
d_fromℕ'60''8243'_62 :: Integer -> Integer -> T__'8739''737'__26 -> T_Fin_10
d_fromℕ'60''8243'_62 Integer
v0 ~Integer
v1 ~T__'8739''737'__26
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)))
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
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)))
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)
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
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
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
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
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)
d_strengthen_144 :: Integer -> T_Fin_10 -> T_Fin_10
d_strengthen_144 :: Integer -> T_Fin_10 -> T_Fin_10
d_strengthen_144 ~Integer
v0 T_Fin_10
v1 = T_Fin_10 -> T_Fin_10
du_strengthen_144 T_Fin_10
v1
du_strengthen_144 :: T_Fin_10 -> T_Fin_10
du_strengthen_144 :: T_Fin_10 -> T_Fin_10
du_strengthen_144 T_Fin_10
v0 = T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0
d_splitAt_152 ::
Integer ->
Integer -> T_Fin_10 -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_splitAt_152 :: Integer -> Integer -> T_Fin_10 -> T__'8846'__30
d_splitAt_152 Integer
v0 ~Integer
v1 T_Fin_10
v2 = Integer -> T_Fin_10 -> T__'8846'__30
du_splitAt_152 Integer
v0 T_Fin_10
v2
du_splitAt_152 ::
Integer -> T_Fin_10 -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_splitAt_152 :: Integer -> T_Fin_10 -> T__'8846'__30
du_splitAt_152 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_152 (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)
d_join_166 ::
Integer ->
Integer -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Fin_10
d_join_166 :: Integer -> Integer -> T__'8846'__30 -> T_Fin_10
d_join_166 Integer
v0 ~Integer
v1 = Integer -> T__'8846'__30 -> T_Fin_10
du_join_166 Integer
v0
du_join_166 ::
Integer -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Fin_10
du_join_166 :: Integer -> T__'8846'__30 -> T_Fin_10
du_join_166 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))
d_quotRem_178 ::
Integer ->
Integer -> T_Fin_10 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_quotRem_178 :: Integer -> Integer -> T_Fin_10 -> T_Σ_14
d_quotRem_178 ~Integer
v0 Integer
v1 T_Fin_10
v2 = Integer -> T_Fin_10 -> T_Σ_14
du_quotRem_178 Integer
v1 T_Fin_10
v2
du_quotRem_178 ::
Integer -> T_Fin_10 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_quotRem_178 :: Integer -> T_Fin_10 -> T_Σ_14
du_quotRem_178 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_178 (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_152 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v1))
d_remQuot_190 ::
Integer ->
Integer -> T_Fin_10 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_remQuot_190 :: Integer -> Integer -> T_Fin_10 -> T_Σ_14
d_remQuot_190 ~Integer
v0 Integer
v1 T_Fin_10
v2 = Integer -> T_Fin_10 -> T_Σ_14
du_remQuot_190 Integer
v1 T_Fin_10
v2
du_remQuot_190 ::
Integer -> T_Fin_10 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_remQuot_190 :: Integer -> T_Fin_10 -> T_Σ_14
du_remQuot_190 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_178 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v1))
d_quotient_196 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d_quotient_196 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d_quotient_196 ~Integer
v0 Integer
v1 T_Fin_10
v2 = Integer -> T_Fin_10 -> T_Fin_10
du_quotient_196 Integer
v1 T_Fin_10
v2
du_quotient_196 :: Integer -> T_Fin_10 -> T_Fin_10
du_quotient_196 :: Integer -> T_Fin_10 -> T_Fin_10
du_quotient_196 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_190 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v1))
d_remainder_202 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d_remainder_202 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d_remainder_202 ~Integer
v0 Integer
v1 T_Fin_10
v2 = Integer -> T_Fin_10 -> T_Fin_10
du_remainder_202 Integer
v1 T_Fin_10
v2
du_remainder_202 :: Integer -> T_Fin_10 -> T_Fin_10
du_remainder_202 :: Integer -> T_Fin_10 -> T_Fin_10
du_remainder_202 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_190 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v1))
d_combine_208 ::
Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_combine_208 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_combine_208 ~Integer
v0 Integer
v1 T_Fin_10
v2 T_Fin_10
v3 = Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_combine_208 Integer
v1 T_Fin_10
v2 T_Fin_10
v3
du_combine_208 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_combine_208 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_combine_208 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_208 (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
d_finToFun_224 ::
Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_finToFun_224 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_finToFun_224 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_196
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'94'__272 (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_224 (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_202
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'94'__272 (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)
d_funToFin_240 ::
Integer -> Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10
d_funToFin_240 :: Integer -> Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10
d_funToFin_240 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_208
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'94'__272 (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_240 (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)))))
d_fold_258 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(Integer -> ()) ->
Integer ->
(Integer -> AgdaAny -> AgdaAny) ->
(Integer -> AgdaAny) -> T_Fin_10 -> AgdaAny
d_fold_258 :: ()
-> (Integer -> ())
-> Integer
-> (Integer -> Any -> Any)
-> (Integer -> Any)
-> T_Fin_10
-> Any
d_fold_258 ~()
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_258 Integer
v2 Integer -> Any -> Any
v3 Integer -> Any
v4 T_Fin_10
v5
du_fold_258 ::
Integer ->
(Integer -> AgdaAny -> AgdaAny) ->
(Integer -> AgdaAny) -> T_Fin_10 -> AgdaAny
du_fold_258 :: Integer
-> (Integer -> Any -> Any) -> (Integer -> Any) -> T_Fin_10 -> Any
du_fold_258 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_258 (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
d_fold'8242'_284 ::
Integer ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(T_Fin_10 -> ()) ->
(T_Fin_10 -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Fin_10 -> AgdaAny
d_fold'8242'_284 :: Integer
-> ()
-> (T_Fin_10 -> ())
-> (T_Fin_10 -> Any -> Any)
-> Any
-> T_Fin_10
-> Any
d_fold'8242'_284 ~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'_284 T_Fin_10 -> Any -> Any
v3 Any
v4 T_Fin_10
v5
du_fold'8242'_284 ::
(T_Fin_10 -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Fin_10 -> AgdaAny
du_fold'8242'_284 :: (T_Fin_10 -> Any -> Any) -> Any -> T_Fin_10 -> Any
du_fold'8242'_284 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'_284 ((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
d_lift_304 ::
Integer ->
Integer ->
Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> T_Fin_10
d_lift_304 :: Integer
-> Integer
-> Integer
-> (T_Fin_10 -> T_Fin_10)
-> T_Fin_10
-> T_Fin_10
d_lift_304 ~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_304 Integer
v2 T_Fin_10 -> T_Fin_10
v3 T_Fin_10
v4
du_lift_304 ::
Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> T_Fin_10
du_lift_304 :: Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> T_Fin_10
du_lift_304 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_304 (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)
d__'43'__324 ::
Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d__'43'__324 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d__'43'__324 ~Integer
v0 ~Integer
v1 T_Fin_10
v2 T_Fin_10
v3 = T_Fin_10 -> T_Fin_10 -> T_Fin_10
du__'43'__324 T_Fin_10
v2 T_Fin_10
v3
du__'43'__324 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du__'43'__324 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du__'43'__324 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'__324 (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
d__'45'__336 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d__'45'__336 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d__'45'__336 ~Integer
v0 T_Fin_10
v1 T_Fin_10
v2 = T_Fin_10 -> T_Fin_10 -> T_Fin_10
du__'45'__336 T_Fin_10
v1 T_Fin_10
v2
du__'45'__336 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du__'45'__336 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du__'45'__336 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'__336 (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
d__ℕ'45'__348 :: Integer -> T_Fin_10 -> T_Fin_10
d__ℕ'45'__348 :: Integer -> T_Fin_10 -> T_Fin_10
d__ℕ'45'__348 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'__348 (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
d__ℕ'45'ℕ__358 :: Integer -> T_Fin_10 -> Integer
d__ℕ'45'ℕ__358 :: Integer -> T_Fin_10 -> Integer
d__ℕ'45'ℕ__358 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'ℕ__358 (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
d_pred_366 :: Integer -> T_Fin_10 -> T_Fin_10
d_pred_366 :: Integer -> T_Fin_10 -> T_Fin_10
d_pred_366 ~Integer
v0 T_Fin_10
v1 = T_Fin_10 -> T_Fin_10
du_pred_366 T_Fin_10
v1
du_pred_366 :: T_Fin_10 -> T_Fin_10
du_pred_366 :: T_Fin_10 -> T_Fin_10
du_pred_366 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
d_opposite_370 :: Integer -> T_Fin_10 -> T_Fin_10
d_opposite_370 :: Integer -> T_Fin_10 -> T_Fin_10
d_opposite_370 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_370 (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)
d_punchOut_382 ::
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_382 :: Integer
-> T_Fin_10
-> T_Fin_10
-> (T__'8801'__12 -> T_Irrelevant_20)
-> T_Fin_10
d_punchOut_382 ~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_382 T_Fin_10
v1 T_Fin_10
v2
du_punchOut_382 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_punchOut_382 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_punchOut_382 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_382 (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
d_punchIn_396 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_punchIn_396 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_punchIn_396 ~Integer
v0 T_Fin_10
v1 T_Fin_10
v2 = T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_punchIn_396 T_Fin_10
v1 T_Fin_10
v2
du_punchIn_396 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_punchIn_396 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_punchIn_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 -> (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_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
d_pinch_406 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_pinch_406 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10
d_pinch_406 ~Integer
v0 T_Fin_10
v1 T_Fin_10
v2 = T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_pinch_406 T_Fin_10
v1 T_Fin_10
v2
du_pinch_406 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_pinch_406 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10
du_pinch_406 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_406 (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
d__'8804'__420 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'8804'__420 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'8804'__420 = Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
forall a. a
erased
d__'8805'__426 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'8805'__426 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'8805'__426 = Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
forall a. a
erased
d__'60'__432 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'60'__432 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'60'__432 = Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
forall a. a
erased
d__'62'__438 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'62'__438 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
d__'62'__438 = Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> ()
forall a. a
erased
d_Ordering_446 :: p -> p -> p -> ()
d_Ordering_446 p
a0 p
a1 p
a2 = ()
data T_Ordering_446
= C_less_454 T_Fin_10 | C_equal_458 | C_greater_464 T_Fin_10
d_compare_470 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Ordering_446
d_compare_470 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Ordering_446
d_compare_470 ~Integer
v0 T_Fin_10
v1 T_Fin_10
v2 = T_Fin_10 -> T_Fin_10 -> T_Ordering_446
du_compare_470 T_Fin_10
v1 T_Fin_10
v2
du_compare_470 :: T_Fin_10 -> T_Fin_10 -> T_Ordering_446
du_compare_470 :: T_Fin_10 -> T_Fin_10 -> T_Ordering_446
du_compare_470 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_446 -> T_Ordering_446
forall a b. a -> b
coe T_Ordering_446
C_equal_458
C_suc_16 T_Fin_10
v4 -> (T_Fin_10 -> T_Ordering_446) -> Any -> T_Ordering_446
forall a b. a -> b
coe T_Fin_10 -> T_Ordering_446
C_less_454 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
C_zero_12)
T_Fin_10
_ -> T_Ordering_446
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_446) -> Any -> T_Ordering_446
forall a b. a -> b
coe T_Fin_10 -> T_Ordering_446
C_greater_464 (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 :: t
v6 = (T_Fin_10 -> T_Fin_10 -> T_Ordering_446) -> Any -> Any -> t
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10 -> T_Ordering_446
du_compare_470 (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_446
forall a b. a -> b
coe
(case Any -> T_Ordering_446
forall a b. a -> b
coe Any
forall a. a
v6 of
C_less_454 T_Fin_10
v8 -> (T_Fin_10 -> T_Ordering_446) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Ordering_446
C_less_454 ((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_446
C_equal_458 -> T_Ordering_446 -> Any
forall a b. a -> b
coe T_Ordering_446
C_equal_458
C_greater_464 T_Fin_10
v8 -> (T_Fin_10 -> T_Ordering_446) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Ordering_446
C_greater_464 ((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_446
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Fin_10
_ -> T_Ordering_446
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Fin_10
_ -> T_Ordering_446
forall a. a
MAlonzo.RTE.mazUnreachableError
d_raise_506 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d_raise_506 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d_raise_506 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
d_inject'43'_512 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d_inject'43'_512 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10
d_inject'43'_512 ~Integer
v0 ~Integer
v1 T_Fin_10
v2 = T_Fin_10 -> T_Fin_10
du_inject'43'_512 T_Fin_10
v2
du_inject'43'_512 :: T_Fin_10 -> T_Fin_10
du_inject'43'_512 :: T_Fin_10 -> T_Fin_10
du_inject'43'_512 T_Fin_10
v0 = T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v0
d__'8826'__518 :: p -> p -> ()
d__'8826'__518 p
a0 p
a1 = ()
newtype T__'8826'__518 = C__'8827'toℕ__524 T_Fin_10