{-# 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.Vec.Bounded.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.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.List.Extrema
import qualified MAlonzo.Code.Data.List.Membership.Setoid
import qualified MAlonzo.Code.Data.List.Relation.Unary.All
import qualified MAlonzo.Code.Data.List.Relation.Unary.All.Properties
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Nat.Properties
import qualified MAlonzo.Code.Data.These.Base
import qualified MAlonzo.Code.Data.Vec.Base
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Nullary
d_max_50 :: Integer -> [Integer] -> Integer
d_max_50 :: Integer -> [Integer] -> Integer
d_max_50
= (T_TotalOrder_652 -> Any -> [Any] -> Any)
-> Any -> Integer -> [Integer] -> Integer
forall a b. a -> b
coe
T_TotalOrder_652 -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Extrema.du_max_128
(T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_1700)
d_xs'8804'max_98 ::
Integer ->
[Integer] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_xs'8804'max_98 :: Integer -> [Integer] -> T_All_44
d_xs'8804'max_98
= (T_TotalOrder_652 -> Any -> [Any] -> T_All_44)
-> Any -> Integer -> [Integer] -> T_All_44
forall a b. a -> b
coe
T_TotalOrder_652 -> Any -> [Any] -> T_All_44
MAlonzo.Code.Data.List.Extrema.du_xs'8804'max_706
(T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_1700)
d_Vec'8804'_122 :: p -> p -> p -> ()
d_Vec'8804'_122 p
a0 p
a1 p
a2 = ()
data T_Vec'8804'_122
= C__'44'__140 Integer MAlonzo.Code.Data.Vec.Base.T_Vec_24
d_length_134 :: T_Vec'8804'_122 -> Integer
d_length_134 :: T_Vec'8804'_122 -> Integer
d_length_134 T_Vec'8804'_122
v0
= case T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
v0 of
C__'44'__140 Integer
v1 T_Vec_24
v2 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
T_Vec'8804'_122
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
d_vec_136 :: T_Vec'8804'_122 -> MAlonzo.Code.Data.Vec.Base.T_Vec_24
d_vec_136 :: T_Vec'8804'_122 -> T_Vec_24
d_vec_136 T_Vec'8804'_122
v0
= case T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
v0 of
C__'44'__140 Integer
v1 T_Vec_24
v2 -> T_Vec_24 -> T_Vec_24
forall a b. a -> b
coe T_Vec_24
v2
T_Vec'8804'_122
_ -> T_Vec_24
forall a. a
MAlonzo.RTE.mazUnreachableError
d_fromVec_144 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Integer -> MAlonzo.Code.Data.Vec.Base.T_Vec_24 -> T_Vec'8804'_122
d_fromVec_144 :: () -> () -> Integer -> T_Vec_24 -> T_Vec'8804'_122
d_fromVec_144 ~()
v0 ~()
v1 Integer
v2 T_Vec_24
v3 = Integer -> T_Vec_24 -> T_Vec'8804'_122
du_fromVec_144 Integer
v2 T_Vec_24
v3
du_fromVec_144 ::
Integer -> MAlonzo.Code.Data.Vec.Base.T_Vec_24 -> T_Vec'8804'_122
du_fromVec_144 :: Integer -> T_Vec_24 -> T_Vec'8804'_122
du_fromVec_144 Integer
v0 T_Vec_24
v1 = (Integer -> T_Vec_24 -> T_Vec'8804'_122)
-> Integer -> T_Vec_24 -> T_Vec'8804'_122
forall a b. a -> b
coe Integer -> T_Vec_24 -> T_Vec'8804'_122
C__'44'__140 Integer
v0 T_Vec_24
v1
d_padRight_150 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Integer ->
AgdaAny -> T_Vec'8804'_122 -> MAlonzo.Code.Data.Vec.Base.T_Vec_24
d_padRight_150 :: () -> () -> Integer -> Any -> T_Vec'8804'_122 -> T_Vec_24
d_padRight_150 ~()
v0 ~()
v1 Integer
v2 Any
v3 T_Vec'8804'_122
v4 = Integer -> Any -> T_Vec'8804'_122 -> T_Vec_24
du_padRight_150 Integer
v2 Any
v3 T_Vec'8804'_122
v4
du_padRight_150 ::
Integer ->
AgdaAny -> T_Vec'8804'_122 -> MAlonzo.Code.Data.Vec.Base.T_Vec_24
du_padRight_150 :: Integer -> Any -> T_Vec'8804'_122 -> T_Vec_24
du_padRight_150 Integer
v0 Any
v1 T_Vec'8804'_122
v2
= case T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
v2 of
C__'44'__140 Integer
v3 T_Vec_24
v4
-> let v6 :: t
v6
= (T_Dec_32 -> Any) -> Any -> t
forall a b. a -> b
coe
T_Dec_32 -> Any
MAlonzo.Code.Relation.Nullary.du_recompute_60
((Integer -> Integer -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T_Dec_32
MAlonzo.Code.Data.Nat.Properties.d__'8804''8243''63'__4756 (Integer -> Any
forall a b. a -> b
coe Integer
v3)
(Integer -> Any
forall a b. a -> b
coe Integer
v0)) in
Any -> T_Vec_24
forall a b. a -> b
coe
(case Any -> T__'8804''8243'__188
forall a b. a -> b
coe Any
forall a. a
v6 of
MAlonzo.Code.Data.Nat.Base.C_less'45'than'45'or'45'equal_202 Integer
v7
-> (T_Vec_24 -> T_Vec_24 -> T_Vec_24) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Vec_24 -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du__'43''43'__190 (T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24
v4)
((Integer -> Any -> T_Vec_24) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Any -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du_replicate_490 (Integer -> Any
forall a b. a -> b
coe Integer
v7) (Any -> Any
forall a b. a -> b
coe Any
v1))
T__'8804''8243'__188
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Vec'8804'_122
_ -> T_Vec_24
forall a. a
MAlonzo.RTE.mazUnreachableError
d_padLeft_170 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Integer ->
AgdaAny -> T_Vec'8804'_122 -> MAlonzo.Code.Data.Vec.Base.T_Vec_24
d_padLeft_170 :: () -> () -> Integer -> Any -> T_Vec'8804'_122 -> T_Vec_24
d_padLeft_170 ~()
v0 ~()
v1 Integer
v2 Any
v3 T_Vec'8804'_122
v4 = Integer -> Any -> T_Vec'8804'_122 -> T_Vec_24
du_padLeft_170 Integer
v2 Any
v3 T_Vec'8804'_122
v4
du_padLeft_170 ::
Integer ->
AgdaAny -> T_Vec'8804'_122 -> MAlonzo.Code.Data.Vec.Base.T_Vec_24
du_padLeft_170 :: Integer -> Any -> T_Vec'8804'_122 -> T_Vec_24
du_padLeft_170 Integer
v0 Any
v1 T_Vec'8804'_122
v2
= case T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
v2 of
C__'44'__140 Integer
v3 T_Vec_24
v4
-> let v6 :: t
v6
= (T_Dec_32 -> Any) -> Any -> t
forall a b. a -> b
coe
T_Dec_32 -> Any
MAlonzo.Code.Relation.Nullary.du_recompute_60
((Integer -> Integer -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T_Dec_32
MAlonzo.Code.Data.Nat.Properties.d__'8804''8243''63'__4756 (Integer -> Any
forall a b. a -> b
coe Integer
v3)
(Integer -> Any
forall a b. a -> b
coe Integer
v0)) in
Any -> T_Vec_24
forall a b. a -> b
coe
(case Any -> T__'8804''8243'__188
forall a b. a -> b
coe Any
forall a. a
v6 of
MAlonzo.Code.Data.Nat.Base.C_less'45'than'45'or'45'equal_202 Integer
v7
-> (T_Vec_24 -> T_Vec_24 -> T_Vec_24) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Vec_24 -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du__'43''43'__190
((Integer -> Any -> T_Vec_24) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Any -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du_replicate_490 (Integer -> Any
forall a b. a -> b
coe Integer
v7) (Any -> Any
forall a b. a -> b
coe Any
v1))
(T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24
v4)
T__'8804''8243'__188
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Vec'8804'_122
_ -> T_Vec_24
forall a. a
MAlonzo.RTE.mazUnreachableError
d_padBoth_238 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Integer ->
AgdaAny ->
AgdaAny -> T_Vec'8804'_122 -> MAlonzo.Code.Data.Vec.Base.T_Vec_24
d_padBoth_238 :: () -> () -> Integer -> Any -> Any -> T_Vec'8804'_122 -> T_Vec_24
d_padBoth_238 ~()
v0 ~()
v1 Integer
v2 Any
v3 Any
v4 T_Vec'8804'_122
v5 = Integer -> Any -> Any -> T_Vec'8804'_122 -> T_Vec_24
du_padBoth_238 Integer
v2 Any
v3 Any
v4 T_Vec'8804'_122
v5
du_padBoth_238 ::
Integer ->
AgdaAny ->
AgdaAny -> T_Vec'8804'_122 -> MAlonzo.Code.Data.Vec.Base.T_Vec_24
du_padBoth_238 :: Integer -> Any -> Any -> T_Vec'8804'_122 -> T_Vec_24
du_padBoth_238 Integer
v0 Any
v1 Any
v2 T_Vec'8804'_122
v3
= case T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
v3 of
C__'44'__140 Integer
v4 T_Vec_24
v5
-> let v7 :: t
v7
= (T_Dec_32 -> Any) -> Any -> t
forall a b. a -> b
coe
T_Dec_32 -> Any
MAlonzo.Code.Relation.Nullary.du_recompute_60
((Integer -> Integer -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T_Dec_32
MAlonzo.Code.Data.Nat.Properties.d__'8804''8243''63'__4756 (Integer -> Any
forall a b. a -> b
coe Integer
v4)
(Integer -> Any
forall a b. a -> b
coe Integer
v0)) in
Any -> T_Vec_24
forall a b. a -> b
coe
(case Any -> T__'8804''8243'__188
forall a b. a -> b
coe Any
forall a. a
v7 of
MAlonzo.Code.Data.Nat.Base.C_less'45'than'45'or'45'equal_202 Integer
v8
-> (T_Vec_24 -> T_Vec_24 -> T_Vec_24) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Vec_24 -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du__'43''43'__190
((Integer -> Any -> T_Vec_24) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Any -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du_replicate_490
((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d_'8970'_'47'2'8971'_126 (Integer -> Any
forall a b. a -> b
coe Integer
v8))
(Any -> Any
forall a b. a -> b
coe Any
v1))
((T_Vec_24 -> T_Vec_24 -> T_Vec_24) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Vec_24 -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du__'43''43'__190 (T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24
v5)
((Integer -> Any -> T_Vec_24) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Any -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du_replicate_490
((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d_'8968'_'47'2'8969'_130 (Integer -> Any
forall a b. a -> b
coe Integer
v8))
(Any -> Any
forall a b. a -> b
coe Any
v2)))
T__'8804''8243'__188
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Vec'8804'_122
_ -> T_Vec_24
forall a. a
MAlonzo.RTE.mazUnreachableError
d_fromList_288 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> [AgdaAny] -> T_Vec'8804'_122
d_fromList_288 :: () -> () -> [Any] -> T_Vec'8804'_122
d_fromList_288 ~()
v0 ~()
v1 [Any]
v2 = [Any] -> T_Vec'8804'_122
du_fromList_288 [Any]
v2
du_fromList_288 :: [AgdaAny] -> T_Vec'8804'_122
du_fromList_288 :: [Any] -> T_Vec'8804'_122
du_fromList_288 [Any]
v0
= (Integer -> T_Vec_24 -> T_Vec'8804'_122)
-> Any -> Any -> T_Vec'8804'_122
forall a b. a -> b
coe
Integer -> T_Vec_24 -> T_Vec'8804'_122
du_fromVec_144 (([Any] -> Integer) -> [Any] -> Any
forall a b. a -> b
coe [Any] -> Integer
MAlonzo.Code.Data.List.Base.du_length_296 [Any]
v0)
(([Any] -> T_Vec_24) -> Any -> Any
forall a b. a -> b
coe [Any] -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du_fromList_660 ([Any] -> Any
forall a b. a -> b
coe [Any]
v0))
d_toList_292 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> Integer -> T_Vec'8804'_122 -> [AgdaAny]
d_toList_292 :: () -> () -> Integer -> T_Vec'8804'_122 -> [Any]
d_toList_292 ~()
v0 ~()
v1 ~Integer
v2 T_Vec'8804'_122
v3 = T_Vec'8804'_122 -> [Any]
du_toList_292 T_Vec'8804'_122
v3
du_toList_292 :: T_Vec'8804'_122 -> [AgdaAny]
du_toList_292 :: T_Vec'8804'_122 -> [Any]
du_toList_292 T_Vec'8804'_122
v0
= (T_Vec_24 -> [Any]) -> Any -> [Any]
forall a b. a -> b
coe
T_Vec_24 -> [Any]
MAlonzo.Code.Data.Vec.Base.du_toList_652 ((T_Vec'8804'_122 -> T_Vec_24) -> Any -> Any
forall a b. a -> b
coe T_Vec'8804'_122 -> T_Vec_24
d_vec_136 (T_Vec'8804'_122 -> Any
forall a b. a -> b
coe T_Vec'8804'_122
v0))
d_replicate_300 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
AgdaAny -> T_Vec'8804'_122
d_replicate_300 :: ()
-> ()
-> Integer
-> Integer
-> T__'8804'__18
-> Any
-> T_Vec'8804'_122
d_replicate_300 ~()
v0 ~()
v1 Integer
v2 ~Integer
v3 ~T__'8804'__18
v4 Any
v5 = Integer -> Any -> T_Vec'8804'_122
du_replicate_300 Integer
v2 Any
v5
du_replicate_300 :: Integer -> AgdaAny -> T_Vec'8804'_122
du_replicate_300 :: Integer -> Any -> T_Vec'8804'_122
du_replicate_300 Integer
v0 Any
v1
= (Integer -> T_Vec_24 -> T_Vec'8804'_122)
-> Integer -> Any -> T_Vec'8804'_122
forall a b. a -> b
coe
Integer -> T_Vec_24 -> T_Vec'8804'_122
C__'44'__140 Integer
v0
((Integer -> Any -> T_Vec_24) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Any -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du_replicate_490 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Any -> Any
forall a b. a -> b
coe Any
v1))
d_'91''93'_308 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> Integer -> T_Vec'8804'_122
d_'91''93'_308 :: () -> () -> Integer -> T_Vec'8804'_122
d_'91''93'_308 ~()
v0 ~()
v1 ~Integer
v2 = T_Vec'8804'_122
du_'91''93'_308
du_'91''93'_308 :: T_Vec'8804'_122
du_'91''93'_308 :: T_Vec'8804'_122
du_'91''93'_308
= (Integer -> T_Vec_24 -> T_Vec'8804'_122)
-> Integer -> Any -> T_Vec'8804'_122
forall a b. a -> b
coe
Integer -> T_Vec_24 -> T_Vec'8804'_122
C__'44'__140 (Integer
0 :: Integer)
(T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24
MAlonzo.Code.Data.Vec.Base.C_'91''93'_28)
d__'8759'__312 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> Integer -> AgdaAny -> T_Vec'8804'_122 -> T_Vec'8804'_122
d__'8759'__312 :: () -> () -> Integer -> Any -> T_Vec'8804'_122 -> T_Vec'8804'_122
d__'8759'__312 ~()
v0 ~()
v1 ~Integer
v2 Any
v3 T_Vec'8804'_122
v4 = Any -> T_Vec'8804'_122 -> T_Vec'8804'_122
du__'8759'__312 Any
v3 T_Vec'8804'_122
v4
du__'8759'__312 :: AgdaAny -> T_Vec'8804'_122 -> T_Vec'8804'_122
du__'8759'__312 :: Any -> T_Vec'8804'_122 -> T_Vec'8804'_122
du__'8759'__312 Any
v0 T_Vec'8804'_122
v1
= case T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
v1 of
C__'44'__140 Integer
v2 T_Vec_24
v3
-> (Integer -> T_Vec_24 -> T_Vec'8804'_122)
-> Integer -> Any -> T_Vec'8804'_122
forall a b. a -> b
coe
Integer -> T_Vec_24 -> T_Vec'8804'_122
C__'44'__140 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v2))
((Any -> T_Vec_24 -> T_Vec_24) -> Any -> T_Vec_24 -> Any
forall a b. a -> b
coe Any -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Any
v0 T_Vec_24
v3)
T_Vec'8804'_122
_ -> T_Vec'8804'_122
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'8804''45'cast_326 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__18 ->
T_Vec'8804'_122 -> T_Vec'8804'_122
d_'8804''45'cast_326 :: ()
-> ()
-> Integer
-> Integer
-> T__'8804'__18
-> T_Vec'8804'_122
-> T_Vec'8804'_122
d_'8804''45'cast_326 ~()
v0 ~()
v1 ~Integer
v2 ~Integer
v3 ~T__'8804'__18
v4 T_Vec'8804'_122
v5
= T_Vec'8804'_122 -> T_Vec'8804'_122
du_'8804''45'cast_326 T_Vec'8804'_122
v5
du_'8804''45'cast_326 :: T_Vec'8804'_122 -> T_Vec'8804'_122
du_'8804''45'cast_326 :: T_Vec'8804'_122 -> T_Vec'8804'_122
du_'8804''45'cast_326 T_Vec'8804'_122
v0 = T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
v0
d_'8801''45'cast_340 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Integer ->
Integer ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
T_Vec'8804'_122 -> T_Vec'8804'_122
d_'8801''45'cast_340 :: ()
-> ()
-> Integer
-> Integer
-> T__'8801'__12
-> T_Vec'8804'_122
-> T_Vec'8804'_122
d_'8801''45'cast_340 ~()
v0 ~()
v1 ~Integer
v2 ~Integer
v3 ~T__'8801'__12
v4 T_Vec'8804'_122
v5
= T_Vec'8804'_122 -> T_Vec'8804'_122
du_'8801''45'cast_340 T_Vec'8804'_122
v5
du_'8801''45'cast_340 :: T_Vec'8804'_122 -> T_Vec'8804'_122
du_'8801''45'cast_340 :: T_Vec'8804'_122 -> T_Vec'8804'_122
du_'8801''45'cast_340 T_Vec'8804'_122
v0 = T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
v0
d_map_346 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122
d_map_346 :: ()
-> ()
-> ()
-> ()
-> (Any -> Any)
-> Integer
-> T_Vec'8804'_122
-> T_Vec'8804'_122
d_map_346 ~()
v0 ~()
v1 ~()
v2 ~()
v3 Any -> Any
v4 ~Integer
v5 T_Vec'8804'_122
v6 = (Any -> Any) -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_map_346 Any -> Any
v4 T_Vec'8804'_122
v6
du_map_346 ::
(AgdaAny -> AgdaAny) -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_map_346 :: (Any -> Any) -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_map_346 Any -> Any
v0 T_Vec'8804'_122
v1
= case T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
v1 of
C__'44'__140 Integer
v2 T_Vec_24
v3
-> (Integer -> T_Vec_24 -> T_Vec'8804'_122)
-> Integer -> Any -> T_Vec'8804'_122
forall a b. a -> b
coe
Integer -> T_Vec_24 -> T_Vec'8804'_122
C__'44'__140 Integer
v2
(((Any -> Any) -> T_Vec_24 -> T_Vec_24) -> Any -> Any -> Any
forall a b. a -> b
coe (Any -> Any) -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du_map_176 ((Any -> Any) -> Any
forall a b. a -> b
coe Any -> Any
v0) (T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24
v3))
T_Vec'8804'_122
_ -> T_Vec'8804'_122
forall a. a
MAlonzo.RTE.mazUnreachableError
d_reverse_356 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122
d_reverse_356 :: () -> () -> Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122
d_reverse_356 ~()
v0 ~()
v1 ~Integer
v2 T_Vec'8804'_122
v3 = T_Vec'8804'_122 -> T_Vec'8804'_122
du_reverse_356 T_Vec'8804'_122
v3
du_reverse_356 :: T_Vec'8804'_122 -> T_Vec'8804'_122
du_reverse_356 :: T_Vec'8804'_122 -> T_Vec'8804'_122
du_reverse_356 T_Vec'8804'_122
v0
= case T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
v0 of
C__'44'__140 Integer
v1 T_Vec_24
v2
-> (Integer -> T_Vec_24 -> T_Vec'8804'_122)
-> Integer -> Any -> T_Vec'8804'_122
forall a b. a -> b
coe
Integer -> T_Vec_24 -> T_Vec'8804'_122
C__'44'__140 Integer
v1 ((T_Vec_24 -> T_Vec_24) -> T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du_reverse_668 T_Vec_24
v2)
T_Vec'8804'_122
_ -> T_Vec'8804'_122
forall a. a
MAlonzo.RTE.mazUnreachableError
d_alignWith_364 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(MAlonzo.Code.Data.These.Base.T_These_38 -> AgdaAny) ->
Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
d_alignWith_364 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (T_These_38 -> Any)
-> Integer
-> T_Vec'8804'_122
-> T_Vec'8804'_122
-> T_Vec'8804'_122
d_alignWith_364 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 T_These_38 -> Any
v6 ~Integer
v7 T_Vec'8804'_122
v8 T_Vec'8804'_122
v9
= (T_These_38 -> Any)
-> T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_alignWith_364 T_These_38 -> Any
v6 T_Vec'8804'_122
v8 T_Vec'8804'_122
v9
du_alignWith_364 ::
(MAlonzo.Code.Data.These.Base.T_These_38 -> AgdaAny) ->
T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_alignWith_364 :: (T_These_38 -> Any)
-> T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_alignWith_364 T_These_38 -> Any
v0 T_Vec'8804'_122
v1 T_Vec'8804'_122
v2
= case T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
v1 of
C__'44'__140 Integer
v3 T_Vec_24
v4
-> case T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
v2 of
C__'44'__140 Integer
v6 T_Vec_24
v7
-> (Integer -> T_Vec_24 -> T_Vec'8804'_122)
-> Integer -> Any -> T_Vec'8804'_122
forall a b. a -> b
coe
Integer -> T_Vec_24 -> T_Vec'8804'_122
C__'44'__140
(Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'8852'__106 (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe Integer
v6))
(((T_These_38 -> Any) -> T_Vec_24 -> T_Vec_24 -> T_Vec_24)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(T_These_38 -> Any) -> T_Vec_24 -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du_alignWith_214 ((T_These_38 -> Any) -> Any
forall a b. a -> b
coe T_These_38 -> Any
v0) (T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24
v4)
(T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24
v7))
T_Vec'8804'_122
_ -> T_Vec'8804'_122
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Vec'8804'_122
_ -> T_Vec'8804'_122
forall a. a
MAlonzo.RTE.mazUnreachableError
d_zipWith_378 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
d_zipWith_378 :: ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (Any -> Any -> Any)
-> Integer
-> T_Vec'8804'_122
-> T_Vec'8804'_122
-> T_Vec'8804'_122
d_zipWith_378 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~()
v5 Any -> Any -> Any
v6 ~Integer
v7 T_Vec'8804'_122
v8 T_Vec'8804'_122
v9
= (Any -> Any -> Any)
-> T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_zipWith_378 Any -> Any -> Any
v6 T_Vec'8804'_122
v8 T_Vec'8804'_122
v9
du_zipWith_378 ::
(AgdaAny -> AgdaAny -> AgdaAny) ->
T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_zipWith_378 :: (Any -> Any -> Any)
-> T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_zipWith_378 Any -> Any -> Any
v0 T_Vec'8804'_122
v1 T_Vec'8804'_122
v2
= case T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
v1 of
C__'44'__140 Integer
v3 T_Vec_24
v4
-> case T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
v2 of
C__'44'__140 Integer
v6 T_Vec_24
v7
-> (Integer -> T_Vec_24 -> T_Vec'8804'_122)
-> Integer -> Any -> T_Vec'8804'_122
forall a b. a -> b
coe
Integer -> T_Vec_24 -> T_Vec'8804'_122
C__'44'__140
(Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'8851'__116 (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe Integer
v6))
(((Any -> Any -> Any) -> T_Vec_24 -> T_Vec_24 -> T_Vec_24)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any) -> T_Vec_24 -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du_restrictWith_238 ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe Any -> Any -> Any
v0) (T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24
v4)
(T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24
v7))
T_Vec'8804'_122
_ -> T_Vec'8804'_122
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Vec'8804'_122
_ -> T_Vec'8804'_122
forall a. a
MAlonzo.RTE.mazUnreachableError
d_zip_392 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
d_zip_392 :: ()
-> ()
-> ()
-> ()
-> Integer
-> T_Vec'8804'_122
-> T_Vec'8804'_122
-> T_Vec'8804'_122
d_zip_392 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~Integer
v4 = T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_zip_392
du_zip_392 :: T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_zip_392 :: T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_zip_392
= ((Any -> Any -> Any)
-> T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122)
-> Any -> T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe
(Any -> Any -> Any)
-> T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_zipWith_378 ((Any -> Any -> T_Σ_14) -> Any
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32)
d_align_396 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
d_align_396 :: ()
-> ()
-> ()
-> ()
-> Integer
-> T_Vec'8804'_122
-> T_Vec'8804'_122
-> T_Vec'8804'_122
d_align_396 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~Integer
v4 = T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_align_396
du_align_396 ::
T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_align_396 :: T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_align_396 = ((T_These_38 -> Any)
-> T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122)
-> Any -> T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe (T_These_38 -> Any)
-> T_Vec'8804'_122 -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_alignWith_364 ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 -> Any
v0))
d_take_402 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> Integer -> Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122
d_take_402 :: ()
-> () -> Integer -> Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122
d_take_402 ~()
v0 ~()
v1 ~Integer
v2 Integer
v3 T_Vec'8804'_122
v4 = Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_take_402 Integer
v3 T_Vec'8804'_122
v4
du_take_402 :: Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_take_402 :: Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_take_402 Integer
v0 T_Vec'8804'_122
v1
= case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
0 -> T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
du_'91''93'_308
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_Vec'8804'_122
forall a b. a -> b
coe
(case T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
v1 of
C__'44'__140 Integer
v3 T_Vec_24
v4
-> case T_Vec_24 -> T_Vec_24
forall a b. a -> b
coe T_Vec_24
v4 of
T_Vec_24
MAlonzo.Code.Data.Vec.Base.C_'91''93'_28 -> T_Vec'8804'_122 -> Any
forall a b. a -> b
coe T_Vec'8804'_122
du_'91''93'_308
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Any
v7 T_Vec_24
v8
-> let v9 :: Integer
v9 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe
((Any -> T_Vec'8804'_122 -> T_Vec'8804'_122) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec'8804'_122 -> T_Vec'8804'_122
du__'8759'__312 (Any -> Any
forall a b. a -> b
coe Any
v7)
((Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122)
-> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_take_402 (Integer -> Any
forall a b. a -> b
coe Integer
v2) ((Integer -> T_Vec_24 -> T_Vec'8804'_122)
-> Integer -> T_Vec_24 -> Any
forall a b. a -> b
coe Integer -> T_Vec_24 -> T_Vec'8804'_122
C__'44'__140 Integer
v9 T_Vec_24
v8)))
T_Vec_24
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Vec'8804'_122
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_drop_422 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> Integer -> Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122
d_drop_422 :: ()
-> () -> Integer -> Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122
d_drop_422 ~()
v0 ~()
v1 ~Integer
v2 Integer
v3 T_Vec'8804'_122
v4 = Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_drop_422 Integer
v3 T_Vec'8804'_122
v4
du_drop_422 :: Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_drop_422 :: Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_drop_422 Integer
v0 T_Vec'8804'_122
v1
= case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
0 -> T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
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_Vec'8804'_122
forall a b. a -> b
coe
(case T_Vec'8804'_122 -> T_Vec'8804'_122
forall a b. a -> b
coe T_Vec'8804'_122
v1 of
C__'44'__140 Integer
v3 T_Vec_24
v4
-> case T_Vec_24 -> T_Vec_24
forall a b. a -> b
coe T_Vec_24
v4 of
T_Vec_24
MAlonzo.Code.Data.Vec.Base.C_'91''93'_28 -> T_Vec'8804'_122 -> Any
forall a b. a -> b
coe T_Vec'8804'_122
du_'91''93'_308
MAlonzo.Code.Data.Vec.Base.C__'8759'__36 Any
v7 T_Vec_24
v8
-> let v9 :: Integer
v9 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe ((Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122)
-> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T_Vec'8804'_122 -> T_Vec'8804'_122
du_drop_422 (Integer -> Any
forall a b. a -> b
coe Integer
v2) ((Integer -> T_Vec_24 -> T_Vec'8804'_122)
-> Integer -> T_Vec_24 -> Any
forall a b. a -> b
coe Integer -> T_Vec_24 -> T_Vec'8804'_122
C__'44'__140 Integer
v9 T_Vec_24
v8))
T_Vec_24
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Vec'8804'_122
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_rectangle_440 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_rectangle_440 :: () -> () -> [T_Σ_14] -> T_Σ_14
d_rectangle_440 ~()
v0 ~()
v1 [T_Σ_14]
v2 = [T_Σ_14] -> T_Σ_14
du_rectangle_440 [T_Σ_14]
v2
du_rectangle_440 ::
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_rectangle_440 :: [T_Σ_14] -> T_Σ_14
du_rectangle_440 [T_Σ_14]
v0
= (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(([T_Σ_14] -> Integer) -> Any -> Any
forall a b. a -> b
coe [T_Σ_14] -> Integer
du_width_452 ([T_Σ_14] -> Any
forall a b. a -> b
coe [T_Σ_14]
v0)) (([T_Σ_14] -> [T_Vec'8804'_122]) -> Any -> Any
forall a b. a -> b
coe [T_Σ_14] -> [T_Vec'8804'_122]
du_padded_458 ([T_Σ_14] -> Any
forall a b. a -> b
coe [T_Σ_14]
v0))
d_sizes_450 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] -> [Integer]
d_sizes_450 :: () -> () -> [T_Σ_14] -> [Integer]
d_sizes_450 ~()
v0 ~()
v1 [T_Σ_14]
v2 = [T_Σ_14] -> [Integer]
du_sizes_450 [T_Σ_14]
v2
du_sizes_450 ::
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] -> [Integer]
du_sizes_450 :: [T_Σ_14] -> [Integer]
du_sizes_450 [T_Σ_14]
v0
= ((Any -> Any) -> [Any] -> [Any]) -> Any -> Any -> [Integer]
forall a b. a -> b
coe
(Any -> Any) -> [Any] -> [Any]
MAlonzo.Code.Data.List.Base.du_map_22
((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v1 -> T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v1)))
([T_Σ_14] -> Any
forall a b. a -> b
coe [T_Σ_14]
v0)
d_width_452 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] -> Integer
d_width_452 :: () -> () -> [T_Σ_14] -> Integer
d_width_452 ~()
v0 ~()
v1 [T_Σ_14]
v2 = [T_Σ_14] -> Integer
du_width_452 [T_Σ_14]
v2
du_width_452 :: [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] -> Integer
du_width_452 :: [T_Σ_14] -> Integer
du_width_452 [T_Σ_14]
v0
= (T_TotalOrder_652 -> Any -> [Any] -> Any)
-> T_TotalOrder_652 -> Integer -> Any -> Integer
forall a b. a -> b
coe
T_TotalOrder_652 -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Extrema.du_max_128
T_TotalOrder_652
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_1700
(Integer
0 :: Integer) (([T_Σ_14] -> [Integer]) -> Any -> Any
forall a b. a -> b
coe [T_Σ_14] -> [Integer]
du_sizes_450 ([T_Σ_14] -> Any
forall a b. a -> b
coe [T_Σ_14]
v0))
d_all'8804'_456 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_all'8804'_456 :: () -> () -> [T_Σ_14] -> T_All_44
d_all'8804'_456 ~()
v0 ~()
v1 [T_Σ_14]
v2 = [T_Σ_14] -> T_All_44
du_all'8804'_456 [T_Σ_14]
v2
du_all'8804'_456 ::
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_all'8804'_456 :: [T_Σ_14] -> T_All_44
du_all'8804'_456 [T_Σ_14]
v0
= ([Any] -> T_All_44 -> T_All_44) -> Any -> Any -> T_All_44
forall a b. a -> b
coe
[Any] -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.Properties.du_map'8315'_688
([T_Σ_14] -> Any
forall a b. a -> b
coe [T_Σ_14]
v0)
((T_TotalOrder_652 -> Any -> [Any] -> T_All_44)
-> T_TotalOrder_652 -> Integer -> Any -> Any
forall a b. a -> b
coe
T_TotalOrder_652 -> Any -> [Any] -> T_All_44
MAlonzo.Code.Data.List.Extrema.du_xs'8804'max_706
T_TotalOrder_652
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_1700
(Integer
0 :: Integer) (([T_Σ_14] -> [Integer]) -> Any -> Any
forall a b. a -> b
coe [T_Σ_14] -> [Integer]
du_sizes_450 ([T_Σ_14] -> Any
forall a b. a -> b
coe [T_Σ_14]
v0)))
d_padded_458 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] -> [T_Vec'8804'_122]
d_padded_458 :: () -> () -> [T_Σ_14] -> [T_Vec'8804'_122]
d_padded_458 ~()
v0 ~()
v1 [T_Σ_14]
v2 = [T_Σ_14] -> [T_Vec'8804'_122]
du_padded_458 [T_Σ_14]
v2
du_padded_458 ::
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] -> [T_Vec'8804'_122]
du_padded_458 :: [T_Σ_14] -> [T_Vec'8804'_122]
du_padded_458 [T_Σ_14]
v0
= (T_Setoid_44 -> [Any] -> (Any -> T_Any_34 -> Any) -> [Any])
-> Any -> Any -> Any -> [T_Vec'8804'_122]
forall a b. a -> b
coe
T_Setoid_44 -> [Any] -> (Any -> T_Any_34 -> Any) -> [Any]
MAlonzo.Code.Data.List.Membership.Setoid.du_mapWith'8712'_58
(T_Setoid_44 -> Any
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
([T_Σ_14] -> Any
forall a b. a -> b
coe [T_Σ_14]
v0)
((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v1 Any
v2 -> T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v1)))