{-# 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.Untyped.Reduction 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.List
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Builtin.Signature
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.List.NonEmpty.Base
import qualified MAlonzo.Code.Data.List.Relation.Unary.All
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.Untyped.CEK
import qualified MAlonzo.Code.Untyped.RenamingSubstitution
d_Arity_4 :: ()
d_Arity_4 = ()
data T_Arity_4 = C_no'45'builtin_6 | C_want_8 Integer Integer
d_want'45'injective'8320'_18 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_want'45'injective'8320'_18 :: Integer
-> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
d_want'45'injective'8320'_18 = Integer
-> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_want'45'injective'8321'_28 ::
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_want'45'injective'8321'_28 :: Integer
-> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
d_want'45'injective'8321'_28 = Integer
-> Integer -> Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_interleave'45'error_32 :: a
d_interleave'45'error_32
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: Untyped.Reduction.interleave-error"
d_sat_36 :: () -> MAlonzo.Code.Untyped.T__'8866'_14 -> T_Arity_4
d_sat_36 :: () -> T__'8866'_14 -> T_Arity_4
d_sat_36 ~()
v0 T__'8866'_14
v1 = T__'8866'_14 -> T_Arity_4
du_sat_36 T__'8866'_14
v1
du_sat_36 :: MAlonzo.Code.Untyped.T__'8866'_14 -> T_Arity_4
du_sat_36 :: T__'8866'_14 -> T_Arity_4
du_sat_36 T__'8866'_14
v0
= case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v0 of
MAlonzo.Code.Untyped.C_'96'_18 AgdaAny
v1 -> T_Arity_4 -> T_Arity_4
forall a b. a -> b
coe T_Arity_4
C_no'45'builtin_6
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v1 -> T_Arity_4 -> T_Arity_4
forall a b. a -> b
coe T_Arity_4
C_no'45'builtin_6
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v1 T__'8866'_14
v2
-> let v3 :: t
v3 = (T__'8866'_14 -> T_Arity_4) -> AgdaAny -> t
forall a b. a -> b
coe T__'8866'_14 -> T_Arity_4
du_sat_36 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v1) in
AgdaAny -> T_Arity_4
forall a b. a -> b
coe
(case AgdaAny -> T_Arity_4
forall a b. a -> b
coe AgdaAny
forall a. a
v3 of
T_Arity_4
C_no'45'builtin_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3
C_want_8 Integer
v4 Integer
v5
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v4 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v5 of
Integer
0 -> (Integer -> Integer -> T_Arity_4) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> T_Arity_4
C_want_8 (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer))
Integer
_ -> let v6 :: Integer
v6 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v5) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe ((Integer -> Integer -> T_Arity_4) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> T_Arity_4
C_want_8 (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v6))
Integer
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
d_interleave'45'error_32 AgdaAny
forall a. a
erased
T_Arity_4
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v1
-> let v2 :: t
v2 = (T__'8866'_14 -> T_Arity_4) -> AgdaAny -> t
forall a b. a -> b
coe T__'8866'_14 -> T_Arity_4
du_sat_36 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v1) in
AgdaAny -> T_Arity_4
forall a b. a -> b
coe
(case AgdaAny -> T_Arity_4
forall a b. a -> b
coe AgdaAny
forall a. a
v2 of
T_Arity_4
C_no'45'builtin_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2
C_want_8 Integer
v3 Integer
v4
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v3 of
Integer
0 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4) (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
d_interleave'45'error_32 AgdaAny
forall a. a
erased)
Integer
_ -> let v5 :: Integer
v5 = 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
AgdaAny -> AgdaAny
forall a b. a -> b
coe ((Integer -> Integer -> T_Arity_4) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> T_Arity_4
C_want_8 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4))
T_Arity_4
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v1 -> T_Arity_4 -> T_Arity_4
forall a b. a -> b
coe T_Arity_4
C_no'45'builtin_6
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v1 -> T_Arity_4 -> T_Arity_4
forall a b. a -> b
coe T_Arity_4
C_no'45'builtin_6
MAlonzo.Code.Untyped.C_constr_34 Integer
v1 [T__'8866'_14]
v2 -> T_Arity_4 -> T_Arity_4
forall a b. a -> b
coe T_Arity_4
C_no'45'builtin_6
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v1 [T__'8866'_14]
v2 -> T_Arity_4 -> T_Arity_4
forall a b. a -> b
coe T_Arity_4
C_no'45'builtin_6
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v1
-> (Integer -> Integer -> T_Arity_4)
-> AgdaAny -> AgdaAny -> T_Arity_4
forall a b. a -> b
coe
Integer -> Integer -> T_Arity_4
C_want_8 ((T_Builtin_2 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Builtin_2 -> Integer
MAlonzo.Code.Builtin.d_arity'8320'_282 (T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v1))
((T_Builtin_2 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Builtin_2 -> Integer
MAlonzo.Code.Builtin.d_arity_286 (T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v1))
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 -> T_Arity_4 -> T_Arity_4
forall a b. a -> b
coe T_Arity_4
C_no'45'builtin_6
T__'8866'_14
_ -> T_Arity_4
forall a. a
MAlonzo.RTE.mazUnreachableError
d_sat'45'app'45'step_114 ::
() ->
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_sat'45'app'45'step_114 :: ()
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8801'__12
-> T__'8801'__12
d_sat'45'app'45'step_114 = ()
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_sat'45'force'45'step_138 ::
() ->
Integer ->
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_sat'45'force'45'step_138 :: ()
-> Integer
-> Integer
-> T__'8866'_14
-> T__'8801'__12
-> T__'8801'__12
d_sat'45'force'45'step_138 = ()
-> Integer
-> Integer
-> T__'8866'_14
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_nat'45'threshold_158 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_nat'45'threshold_158 :: Integer
-> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12
d_nat'45'threshold_158 = Integer
-> Integer -> T__'8804'__22 -> T__'8804'__22 -> T__'8801'__12
forall a. a
erased
d_Value_182 :: p -> p -> ()
d_Value_182 p
a0 p
a1 = ()
data T_Value_182
= C_delay_188 | C_ƛ_192 | C_con_196 | C_builtin_200 |
C_unsat'8320'_208 Integer Integer T_Value_182 |
C_unsat'8320''8331''8321'_214 Integer T_Value_182 |
C_unsat'8321'_222 Integer T_Value_182 T_Value_182 |
C_constr_228 MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_value'45'constr'45'recurse_234 ::
() ->
Integer ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
T_Value_182 -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_value'45'constr'45'recurse_234 :: () -> Integer -> [T__'8866'_14] -> T_Value_182 -> T_All_44
d_value'45'constr'45'recurse_234 ~()
v0 ~Integer
v1 ~[T__'8866'_14]
v2 T_Value_182
v3
= T_Value_182 -> T_All_44
du_value'45'constr'45'recurse_234 T_Value_182
v3
du_value'45'constr'45'recurse_234 ::
T_Value_182 -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_value'45'constr'45'recurse_234 :: T_Value_182 -> T_All_44
du_value'45'constr'45'recurse_234 T_Value_182
v0
= case T_Value_182 -> T_Value_182
forall a b. a -> b
coe T_Value_182
v0 of
C_constr_228 T_All_44
v3
-> case T_All_44 -> T_All_44
forall a b. a -> b
coe T_All_44
v3 of
T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.C_'91''93'_50 -> T_All_44 -> T_All_44
forall a b. a -> b
coe T_All_44
v3
MAlonzo.Code.Data.List.Relation.Unary.All.C__'8759'__60 AgdaAny
v6 T_All_44
v7
-> (AgdaAny -> T_All_44 -> T_All_44)
-> AgdaAny -> T_All_44 -> T_All_44
forall a b. a -> b
coe
AgdaAny -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.C__'8759'__60 AgdaAny
v6 T_All_44
v7
T_All_44
_ -> T_All_44
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Value_182
_ -> T_All_44
forall a. a
MAlonzo.RTE.mazUnreachableError
d_iterApp_242 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
MAlonzo.Code.Untyped.T__'8866'_14
d_iterApp_242 :: () -> T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
d_iterApp_242 ~()
v0 T__'8866'_14
v1 [T__'8866'_14]
v2 = T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
du_iterApp_242 T__'8866'_14
v1 [T__'8866'_14]
v2
du_iterApp_242 ::
MAlonzo.Code.Untyped.T__'8866'_14 ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
MAlonzo.Code.Untyped.T__'8866'_14
du_iterApp_242 :: T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
du_iterApp_242 T__'8866'_14
v0 [T__'8866'_14]
v1
= case [T__'8866'_14] -> [AgdaAny]
forall a b. a -> b
coe [T__'8866'_14]
v1 of
[] -> T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v0
(:) AgdaAny
v2 [AgdaAny]
v3
-> (T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
du_iterApp_242
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
[AgdaAny]
_ -> T__'8866'_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_reduceBuiltin_252 :: a
d_reduceBuiltin_252
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: Untyped.Reduction.reduceBuiltin"
d__'10230'__256 :: p -> p -> p -> ()
d__'10230'__256 p
a0 p
a1 p
a2 = ()
data T__'10230'__256
= C_ξ'8321'_266 T__'10230'__256 |
C_ξ'8322'_274 T_Value_182 T__'10230'__256 |
C_ξ'8323'_280 T__'10230'__256 | C_β_286 T_Value_182 |
C_force'45'delay_290 | C_error'8321'_294 | C_error'8322'_298 |
C_force'45'error_300 | C_sat'45'app'45'builtin_306 |
C_sat'45'force'45'builtin_310 |
C_case'45'constr_320 MAlonzo.Code.Untyped.T__'8866'_14 |
C_broken'45'const_328 | C_constr'45'step_338 T__'10230'__256 |
C_constr'45'sub'45'step_348 T__'10230'__256 |
C_constr'45'error_354 |
C_constr'45'sub'45'error_362 T__'10230'__256 | C_force'45'ƛ_366 |
C_force'45'con_370 | C_force'45'constr_376 |
C_force'45'interleave'45'error_382 Integer |
C_app'45'interleave'45'error_392 Integer Integer |
C_app'45'con_398 | C_app'45'delay_404 | C_app'45'constr_412 |
C_case'45'error_416 | C_case'45'ƛ_422 | C_case'45'delay_428 |
C_case'45'con_434 | C_case'45'builtin_440 |
C_case'45'unsat'8320'_450 Integer Integer |
C_case'45'unsat'8321'_458 Integer |
C_case'45'reduce_466 T__'10230'__256
d__'10230''42'__470 :: p -> p -> p -> ()
d__'10230''42'__470 p
a0 p
a1 p
a2 = ()
data T__'10230''42'__470
= C_refl_476 |
C_trans_484 MAlonzo.Code.Untyped.T__'8866'_14 T__'10230'__256
T__'10230''42'__470
d_tran'45''10230''42'_494 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
T__'10230''42'__470 -> T__'10230''42'__470 -> T__'10230''42'__470
d_tran'45''10230''42'_494 :: ()
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'10230''42'__470
-> T__'10230''42'__470
-> T__'10230''42'__470
d_tran'45''10230''42'_494 ~()
v0 ~T__'8866'_14
v1 ~T__'8866'_14
v2 ~T__'8866'_14
v3 T__'10230''42'__470
v4 T__'10230''42'__470
v5
= T__'10230''42'__470 -> T__'10230''42'__470 -> T__'10230''42'__470
du_tran'45''10230''42'_494 T__'10230''42'__470
v4 T__'10230''42'__470
v5
du_tran'45''10230''42'_494 ::
T__'10230''42'__470 -> T__'10230''42'__470 -> T__'10230''42'__470
du_tran'45''10230''42'_494 :: T__'10230''42'__470 -> T__'10230''42'__470 -> T__'10230''42'__470
du_tran'45''10230''42'_494 T__'10230''42'__470
v0 T__'10230''42'__470
v1
= case T__'10230''42'__470 -> T__'10230''42'__470
forall a b. a -> b
coe T__'10230''42'__470
v0 of
T__'10230''42'__470
C_refl_476 -> T__'10230''42'__470 -> T__'10230''42'__470
forall a b. a -> b
coe T__'10230''42'__470
v1
C_trans_484 T__'8866'_14
v3 T__'10230'__256
v5 T__'10230''42'__470
v6
-> case T__'10230''42'__470 -> T__'10230''42'__470
forall a b. a -> b
coe T__'10230''42'__470
v1 of
T__'10230''42'__470
C_refl_476 -> (T__'8866'_14
-> T__'10230'__256 -> T__'10230''42'__470 -> T__'10230''42'__470)
-> T__'8866'_14
-> T__'10230'__256
-> T__'10230''42'__470
-> T__'10230''42'__470
forall a b. a -> b
coe T__'8866'_14
-> T__'10230'__256 -> T__'10230''42'__470 -> T__'10230''42'__470
C_trans_484 T__'8866'_14
v3 T__'10230'__256
v5 T__'10230''42'__470
v6
C_trans_484 T__'8866'_14
v8 T__'10230'__256
v10 T__'10230''42'__470
v11
-> (T__'8866'_14
-> T__'10230'__256 -> T__'10230''42'__470 -> T__'10230''42'__470)
-> T__'8866'_14
-> T__'10230'__256
-> AgdaAny
-> T__'10230''42'__470
forall a b. a -> b
coe
T__'8866'_14
-> T__'10230'__256 -> T__'10230''42'__470 -> T__'10230''42'__470
C_trans_484 T__'8866'_14
v3 T__'10230'__256
v5
((T__'10230''42'__470 -> T__'10230''42'__470 -> T__'10230''42'__470)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230''42'__470 -> T__'10230''42'__470 -> T__'10230''42'__470
du_tran'45''10230''42'_494 (T__'10230''42'__470 -> AgdaAny
forall a b. a -> b
coe T__'10230''42'__470
v6) ((T__'8866'_14
-> T__'10230'__256 -> T__'10230''42'__470 -> T__'10230''42'__470)
-> T__'8866'_14
-> T__'10230'__256
-> T__'10230''42'__470
-> AgdaAny
forall a b. a -> b
coe T__'8866'_14
-> T__'10230'__256 -> T__'10230''42'__470 -> T__'10230''42'__470
C_trans_484 T__'8866'_14
v8 T__'10230'__256
v10 T__'10230''42'__470
v11))
T__'10230''42'__470
_ -> T__'10230''42'__470
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'10230''42'__470
_ -> T__'10230''42'__470
forall a. a
MAlonzo.RTE.mazUnreachableError
d_Progress_514 :: p -> p -> ()
d_Progress_514 p
a0 p
a1 = ()
data T_Progress_514
= C_step_522 MAlonzo.Code.Untyped.T__'8866'_14 T__'10230'__256 |
C_done_526 T_Value_182 | C_fail_528
d_progress_532 ::
MAlonzo.Code.Untyped.T__'8866'_14 -> T_Progress_514
d_progress_532 :: T__'8866'_14 -> T_Progress_514
d_progress_532 T__'8866'_14
v0
= case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v0 of
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v1 -> (T_Value_182 -> T_Progress_514) -> AgdaAny -> T_Progress_514
forall a b. a -> b
coe T_Value_182 -> T_Progress_514
C_done_526 (T_Value_182 -> AgdaAny
forall a b. a -> b
coe T_Value_182
C_ƛ_192)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v1 T__'8866'_14
v2
-> let v3 :: T_Progress_514
v3 = T__'8866'_14 -> T_Progress_514
d_progress_532 (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1) in
AgdaAny -> T_Progress_514
forall a b. a -> b
coe
(case T_Progress_514 -> T_Progress_514
forall a b. a -> b
coe T_Progress_514
v3 of
C_step_522 T__'8866'_14
v5 T__'10230'__256
v6
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v5) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
((T__'10230'__256 -> T__'10230'__256) -> T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_ξ'8321'_266 T__'10230'__256
v6)
C_done_526 T_Value_182
v5
-> let v6 :: T_Progress_514
v6 = T__'8866'_14 -> T_Progress_514
d_progress_532 (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case T_Progress_514 -> T_Progress_514
forall a b. a -> b
coe T_Progress_514
v6 of
C_step_522 T__'8866'_14
v8 T__'10230'__256
v9
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v1) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v8))
((T_Value_182 -> T__'10230'__256 -> T__'10230'__256)
-> T_Value_182 -> T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T_Value_182 -> T__'10230'__256 -> T__'10230'__256
C_ξ'8322'_274 T_Value_182
v5 T__'10230'__256
v9)
C_done_526 T_Value_182
v8
-> case T_Value_182 -> T_Value_182
forall a b. a -> b
coe T_Value_182
v5 of
T_Value_182
C_delay_188
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_app'45'delay_404)
T_Value_182
C_ƛ_192
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v10
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.RenamingSubstitution.du__'91'_'93'_468
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v10) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
((T_Value_182 -> T__'10230'__256) -> T_Value_182 -> AgdaAny
forall a b. a -> b
coe T_Value_182 -> T__'10230'__256
C_β_286 T_Value_182
v8)
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Value_182
C_con_196
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_app'45'con_398)
T_Value_182
C_builtin_200
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v10
-> let v11 :: Integer
v11
= Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(((AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> Integer
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_216
(let v11 :: a -> Integer
v11
= \ a
v11 ->
Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(a -> Integer
forall a b. a -> b
coe a
v11) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe ((AgdaAny -> AgdaAny -> Integer) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v12 -> AgdaAny -> Integer
forall {a}. a -> Integer
v11)))
(Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer))
((T_List'8314'_22 -> [AgdaAny]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_List'8314'_22 -> [AgdaAny]
MAlonzo.Code.Data.List.NonEmpty.Base.d_tail_32
((T_Sig_68 -> T_List'8314'_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Sig_68 -> T_List'8314'_22
MAlonzo.Code.Builtin.Signature.d_args_82
((T_Builtin_2 -> T_Sig_68) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Builtin_2 -> T_Sig_68
MAlonzo.Code.Builtin.d_signature_280
(T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v10))))) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v12 :: Integer
v12
= Integer -> Integer -> Integer
addInt
((T_Sig_68 -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe
T_Sig_68 -> Integer
MAlonzo.Code.Builtin.Signature.d_fv'9839'_80
((T_Builtin_2 -> T_Sig_68) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Builtin_2 -> T_Sig_68
MAlonzo.Code.Builtin.d_signature_280
(T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v10)))
((T_Sig_68 -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe
T_Sig_68 -> Integer
MAlonzo.Code.Builtin.Signature.d_fv'8902'_78
((T_Builtin_2 -> T_Sig_68) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Builtin_2 -> T_Sig_68
MAlonzo.Code.Builtin.d_signature_280
(T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v10))) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v12 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v11 of
Integer
1 -> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252 AgdaAny
forall a. a
erased T__'8866'_14
v0)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_sat'45'app'45'builtin_306)
Integer
_ -> let v13 :: Integer
v13
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v11)
(Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_Value_182 -> T_Progress_514) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Value_182 -> T_Progress_514
C_done_526
((Integer -> T_Value_182 -> T_Value_182 -> T_Value_182)
-> Integer -> T_Value_182 -> T_Value_182 -> AgdaAny
forall a b. a -> b
coe
Integer -> T_Value_182 -> T_Value_182 -> T_Value_182
C_unsat'8321'_222 Integer
v13 T_Value_182
v5
T_Value_182
v8))
Integer
_ -> let v13 :: Integer
v13
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v12)
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> Integer -> T__'10230'__256)
-> Integer -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392
Integer
v13 Integer
v11))))
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
C_unsat'8320'_208 Integer
v10 Integer
v11 T_Value_182
v13
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> Integer -> T__'10230'__256)
-> Integer -> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392 Integer
v10 Integer
v11)
C_unsat'8320''8331''8321'_214 Integer
v10 T_Value_182
v12
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v13
-> let v14 :: t
v14 = (T__'8866'_14 -> T_Arity_4) -> AgdaAny -> t
forall a b. a -> b
coe T__'8866'_14 -> T_Arity_4
du_sat_36 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v13) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Arity_4
forall a b. a -> b
coe AgdaAny
forall a. a
v14 of
T_Arity_4
C_no'45'builtin_6
-> case AgdaAny -> T_Arity_4
forall a b. a -> b
coe AgdaAny
forall a. a
v14 of
T_Arity_4
C_no'45'builtin_6
-> ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
AgdaAny
forall a. a
erased
C_want_8 Integer
v15 Integer
v16
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v15 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v16 of
Integer
0 -> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased T__'8866'_14
v1)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_ξ'8321'_266
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'force'45'builtin_310))
Integer
1 -> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased T__'8866'_14
v0)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306)
Integer
_ -> let v17 :: Integer
v17
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v16)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
2 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_Value_182 -> T_Progress_514) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Value_182 -> T_Progress_514
C_done_526
((Integer -> T_Value_182 -> T_Value_182 -> T_Value_182)
-> Integer -> T_Value_182 -> T_Value_182 -> AgdaAny
forall a b. a -> b
coe
Integer -> T_Value_182 -> T_Value_182 -> T_Value_182
C_unsat'8321'_222
Integer
v17 T_Value_182
v5 T_Value_182
v8))
Integer
_ -> let v17 :: Integer
v17
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v15)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
1 :: Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> Integer -> T__'10230'__256)
-> Integer -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392
Integer
v17 Integer
v16))
T_Arity_4
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
C_want_8 Integer
v15 Integer
v16
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v15 of
Integer
0 -> let v17 :: b
v17
= AgdaAny -> b -> b
forall a b. a -> b -> b
seq
(Integer -> AgdaAny
forall a b. a -> b
coe Integer
v16)
(AgdaAny -> AgdaAny -> b
forall a b. a -> b
coe
AgdaAny
forall a. a
d_interleave'45'error_32
AgdaAny
forall a. a
erased) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Arity_4
forall a b. a -> b
coe AgdaAny
forall a. a
v17 of
T_Arity_4
C_no'45'builtin_6
-> ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
AgdaAny
forall a. a
erased
C_want_8 Integer
v18 Integer
v19
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v18 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v19 of
Integer
0 -> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v1)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_ξ'8321'_266
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'force'45'builtin_310))
Integer
1 -> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v0)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306)
Integer
_ -> let v20 :: Integer
v20
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe
Integer
v19)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
2 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_Value_182 -> T_Progress_514) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Value_182 -> T_Progress_514
C_done_526
((Integer -> T_Value_182 -> T_Value_182 -> T_Value_182)
-> Integer -> T_Value_182 -> T_Value_182 -> AgdaAny
forall a b. a -> b
coe
Integer -> T_Value_182 -> T_Value_182 -> T_Value_182
C_unsat'8321'_222
Integer
v20 T_Value_182
v5
T_Value_182
v8))
Integer
_ -> let v20 :: Integer
v20
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v18)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
1 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> Integer -> T__'10230'__256)
-> Integer -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392
Integer
v20 Integer
v19))
T_Arity_4
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
Integer
1 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v16 of
Integer
0 -> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased T__'8866'_14
v1)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_ξ'8321'_266
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'force'45'builtin_310))
Integer
1 -> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252 AgdaAny
forall a. a
erased
T__'8866'_14
v0)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306)
Integer
_ -> let v17 :: Integer
v17
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v16)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
2 :: Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_Value_182 -> T_Progress_514) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Value_182 -> T_Progress_514
C_done_526
((Integer -> T_Value_182 -> T_Value_182 -> T_Value_182)
-> Integer -> T_Value_182 -> T_Value_182 -> AgdaAny
forall a b. a -> b
coe
Integer -> T_Value_182 -> T_Value_182 -> T_Value_182
C_unsat'8321'_222 Integer
v17
T_Value_182
v5 T_Value_182
v8))
Integer
_ -> let v17 :: Integer
v17
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v15)
(Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> Integer -> T__'10230'__256)
-> Integer -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392
Integer
v17 Integer
v16))
T_Arity_4
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
C_unsat'8321'_222 Integer
v11 T_Value_182
v13 T_Value_182
v14
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v15 T__'8866'_14
v16
-> let v17 :: t
v17 = (T__'8866'_14 -> T_Arity_4) -> AgdaAny -> t
forall a b. a -> b
coe T__'8866'_14 -> T_Arity_4
du_sat_36 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v15) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Arity_4
forall a b. a -> b
coe AgdaAny
forall a. a
v17 of
T_Arity_4
C_no'45'builtin_6
-> case AgdaAny -> T_Arity_4
forall a b. a -> b
coe AgdaAny
forall a. a
v17 of
T_Arity_4
C_no'45'builtin_6
-> ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
AgdaAny
forall a. a
erased
C_want_8 Integer
v18 Integer
v19
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v18 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v19 of
Integer
0 -> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased T__'8866'_14
v1)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_ξ'8321'_266
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306))
Integer
1 -> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased T__'8866'_14
v0)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306)
Integer
_ -> let v20 :: Integer
v20
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v19)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
2 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_Value_182 -> T_Progress_514) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Value_182 -> T_Progress_514
C_done_526
((Integer -> T_Value_182 -> T_Value_182 -> T_Value_182)
-> Integer -> T_Value_182 -> T_Value_182 -> AgdaAny
forall a b. a -> b
coe
Integer -> T_Value_182 -> T_Value_182 -> T_Value_182
C_unsat'8321'_222
Integer
v20 T_Value_182
v5 T_Value_182
v8))
Integer
_ -> let v20 :: Integer
v20
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v18)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
1 :: Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> Integer -> T__'10230'__256)
-> Integer -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392
Integer
v20 Integer
v19))
T_Arity_4
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
C_want_8 Integer
v18 Integer
v19
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v18 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v19 of
Integer
0 -> let v20 :: Integer
v20 = Integer
0 :: Integer in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v21 :: Integer
v21 = Integer
0 :: Integer in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v20 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v21 of
Integer
0 -> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v1)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_ξ'8321'_266
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306))
Integer
1 -> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v0)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306)
Integer
_ -> let v22 :: Integer
v22
= -Integer
2 ::
Integer in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_Value_182 -> T_Progress_514) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Value_182 -> T_Progress_514
C_done_526
((Integer -> T_Value_182 -> T_Value_182 -> T_Value_182)
-> Integer -> T_Value_182 -> T_Value_182 -> AgdaAny
forall a b. a -> b
coe
Integer -> T_Value_182 -> T_Value_182 -> T_Value_182
C_unsat'8321'_222
Integer
v22
T_Value_182
v5
T_Value_182
v8))
Integer
_ -> let v22 :: Integer
v22
= -Integer
1 ::
Integer in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> Integer -> T__'10230'__256)
-> Integer -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392
Integer
v22
Integer
v21))))
Integer
_ -> let v20 :: Integer
v20
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v19)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
1 :: Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v21 :: Integer
v21 = Integer
0 :: Integer in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v21 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v19 of
Integer
1 -> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v1)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_ξ'8321'_266
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306))
Integer
2 -> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v0)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306)
Integer
_ -> let v22 :: Integer
v22
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe
Integer
v19)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
3 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_Value_182 -> T_Progress_514) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Value_182 -> T_Progress_514
C_done_526
((Integer -> T_Value_182 -> T_Value_182 -> T_Value_182)
-> Integer -> T_Value_182 -> T_Value_182 -> AgdaAny
forall a b. a -> b
coe
Integer -> T_Value_182 -> T_Value_182 -> T_Value_182
C_unsat'8321'_222
Integer
v22
T_Value_182
v5
T_Value_182
v8))
Integer
_ -> let v22 :: Integer
v22
= -Integer
1 ::
Integer in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> Integer -> T__'10230'__256)
-> Integer -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392
Integer
v22
Integer
v20))))
Integer
_ -> let v20 :: t
v20
= AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
AgdaAny
forall a. a
d_interleave'45'error_32
AgdaAny
forall a. a
erased in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Arity_4
forall a b. a -> b
coe AgdaAny
forall a. a
v20 of
T_Arity_4
C_no'45'builtin_6
-> ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
AgdaAny
forall a. a
erased
C_want_8 Integer
v21 Integer
v22
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v21 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v22 of
Integer
0 -> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v1)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_ξ'8321'_266
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306))
Integer
1 -> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v0)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306)
Integer
_ -> let v23 :: Integer
v23
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe
Integer
v22)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
2 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_Value_182 -> T_Progress_514) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Value_182 -> T_Progress_514
C_done_526
((Integer -> T_Value_182 -> T_Value_182 -> T_Value_182)
-> Integer -> T_Value_182 -> T_Value_182 -> AgdaAny
forall a b. a -> b
coe
Integer -> T_Value_182 -> T_Value_182 -> T_Value_182
C_unsat'8321'_222
Integer
v23 T_Value_182
v5
T_Value_182
v8))
Integer
_ -> let v23 :: Integer
v23
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v21)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
1 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> Integer -> T__'10230'__256)
-> Integer -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392
Integer
v23 Integer
v22))
T_Arity_4
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Arity_4
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
C_constr_228 T_All_44
v11
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_app'45'constr_412)
T_Value_182
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Progress_514
C_fail_528
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_error'8322'_298)
T_Progress_514
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Progress_514
C_fail_528
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_error'8321'_294)
T_Progress_514
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v1
-> let v2 :: T_Progress_514
v2 = T__'8866'_14 -> T_Progress_514
d_progress_532 (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1) in
AgdaAny -> T_Progress_514
forall a b. a -> b
coe
(case T_Progress_514 -> T_Progress_514
forall a b. a -> b
coe T_Progress_514
v2 of
C_step_522 T__'8866'_14
v4 T__'10230'__256
v5
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 ((T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_force_24 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v4))
((T__'10230'__256 -> T__'10230'__256) -> T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_ξ'8323'_280 T__'10230'__256
v5)
C_done_526 T_Value_182
v4
-> let v5 :: t
v5 = (T__'8866'_14 -> T_Arity_4) -> AgdaAny -> t
forall a b. a -> b
coe T__'8866'_14 -> T_Arity_4
du_sat_36 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v1) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Arity_4
forall a b. a -> b
coe AgdaAny
forall a. a
v5 of
T_Arity_4
C_no'45'builtin_6
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v6
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_force'45'ƛ_366)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v6 T__'8866'_14
v7
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Value_182 -> AgdaAny
forall a b. a -> b
coe T_Value_182
v4)
(((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
AgdaAny
forall a. a
erased)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v6
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Value_182 -> AgdaAny
forall a b. a -> b
coe T_Value_182
v4)
(((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
AgdaAny
forall a. a
erased)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v6
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> T__'8866'_14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 T__'8866'_14
v6 (T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_force'45'delay_290)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v6
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_force'45'con_370)
MAlonzo.Code.Untyped.C_constr_34 Integer
v6 [T__'8866'_14]
v7
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_force'45'constr_376)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> T__'8866'_14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 T__'8866'_14
v1 (T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_force'45'error_300)
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
C_want_8 Integer
v6 Integer
v7
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v6 of
Integer
0 -> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> T__'10230'__256) -> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> T__'10230'__256
C_force'45'interleave'45'error_382 Integer
v7)
Integer
1 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v7 of
Integer
0 -> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
d_reduceBuiltin_252 AgdaAny
forall a. a
erased T__'8866'_14
v0)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_sat'45'force'45'builtin_310)
Integer
_ -> let v8 :: Integer
v8 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v7) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_Value_182 -> T_Progress_514) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Value_182 -> T_Progress_514
C_done_526
((Integer -> T_Value_182 -> T_Value_182)
-> Integer -> T_Value_182 -> AgdaAny
forall a b. a -> b
coe Integer -> T_Value_182 -> T_Value_182
C_unsat'8320''8331''8321'_214 Integer
v8 T_Value_182
v4))
Integer
_ -> let v8 :: Integer
v8 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v6) (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe ((T_Value_182 -> T_Progress_514) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Value_182 -> T_Progress_514
C_done_526 ((Integer -> Integer -> T_Value_182 -> T_Value_182)
-> Integer -> Integer -> T_Value_182 -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> T_Value_182 -> T_Value_182
C_unsat'8320'_208 Integer
v8 Integer
v7 T_Value_182
v4))
T_Arity_4
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Progress_514
C_fail_528
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_force'45'error_300)
T_Progress_514
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v1
-> (T_Value_182 -> T_Progress_514) -> AgdaAny -> T_Progress_514
forall a b. a -> b
coe T_Value_182 -> T_Progress_514
C_done_526 (T_Value_182 -> AgdaAny
forall a b. a -> b
coe T_Value_182
C_delay_188)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v1 -> (T_Value_182 -> T_Progress_514) -> AgdaAny -> T_Progress_514
forall a b. a -> b
coe T_Value_182 -> T_Progress_514
C_done_526 (T_Value_182 -> AgdaAny
forall a b. a -> b
coe T_Value_182
C_con_196)
MAlonzo.Code.Untyped.C_constr_34 Integer
v1 [T__'8866'_14]
v2
-> case [T__'8866'_14] -> [AgdaAny]
forall a b. a -> b
coe [T__'8866'_14]
v2 of
[]
-> (T_Value_182 -> T_Progress_514) -> AgdaAny -> T_Progress_514
forall a b. a -> b
coe
T_Value_182 -> T_Progress_514
C_done_526
((T_All_44 -> T_Value_182) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_All_44 -> T_Value_182
C_constr_228
(T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.C_'91''93'_50))
(:) AgdaAny
v3 [AgdaAny]
v4
-> let v5 :: T_Progress_514
v5 = T__'8866'_14 -> T_Progress_514
d_progress_532 (AgdaAny -> T__'8866'_14
forall a b. a -> b
coe AgdaAny
v3) in
AgdaAny -> T_Progress_514
forall a b. a -> b
coe
(case T_Progress_514 -> T_Progress_514
forall a b. a -> b
coe T_Progress_514
v5 of
C_step_522 T__'8866'_14
v7 T__'10230'__256
v8
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((Integer -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Integer -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_constr_34 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1)
((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v7) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4)))
((T__'10230'__256 -> T__'10230'__256) -> T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_constr'45'step_338 T__'10230'__256
v8)
C_done_526 T_Value_182
v7
-> let v8 :: T_Progress_514
v8
= T__'8866'_14 -> T_Progress_514
d_progress_532
((Integer -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe Integer -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_constr_34 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case T_Progress_514 -> T_Progress_514
forall a b. a -> b
coe T_Progress_514
v8 of
C_step_522 T__'8866'_14
v10 T__'10230'__256
v11
-> case T__'10230'__256 -> T__'10230'__256
forall a b. a -> b
coe T__'10230'__256
v11 of
C_constr'45'step_338 T__'10230'__256
v16
-> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v4 of
(:) AgdaAny
v17 [AgdaAny]
v18
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v10 of
MAlonzo.Code.Untyped.C_constr_34 Integer
v19 [T__'8866'_14]
v20
-> case [T__'8866'_14] -> [AgdaAny]
forall a b. a -> b
coe [T__'8866'_14]
v20 of
(:) AgdaAny
v21 [AgdaAny]
v22
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((Integer -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Integer -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_constr_34
(Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1)
((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v21) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v18))))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_constr'45'sub'45'step_348
((T__'10230'__256 -> T__'10230'__256) -> T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_constr'45'step_338 T__'10230'__256
v16))
[AgdaAny]
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
[AgdaAny]
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
C_constr'45'sub'45'step_348 T__'10230'__256
v16
-> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v4 of
(:) AgdaAny
v17 [AgdaAny]
v18
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v10 of
MAlonzo.Code.Untyped.C_constr_34 Integer
v19 [T__'8866'_14]
v20
-> case [T__'8866'_14] -> [AgdaAny]
forall a b. a -> b
coe [T__'8866'_14]
v20 of
(:) AgdaAny
v21 [AgdaAny]
v22
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((Integer -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Integer -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_constr_34
(Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1)
((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v17) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v22))))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_constr'45'sub'45'step_348
((T__'10230'__256 -> T__'10230'__256) -> T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_constr'45'sub'45'step_348
T__'10230'__256
v16))
[AgdaAny]
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
[AgdaAny]
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'10230'__256
C_constr'45'error_354
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_constr'45'sub'45'error_362
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_constr'45'error_354))
C_constr'45'sub'45'error_362 T__'10230'__256
v15
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_constr'45'sub'45'error_362
((T__'10230'__256 -> T__'10230'__256) -> T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_constr'45'sub'45'error_362 T__'10230'__256
v15))
T__'10230'__256
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
C_done_526 T_Value_182
v10
-> (T_Value_182 -> T_Progress_514) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Value_182 -> T_Progress_514
C_done_526
((T_All_44 -> T_Value_182) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_All_44 -> T_Value_182
C_constr_228
((AgdaAny -> T_All_44 -> T_All_44)
-> T_Value_182 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.C__'8759'__60
T_Value_182
v7 ((T_Value_182 -> T_All_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Value_182 -> T_All_44
du_value'45'constr'45'recurse_234 (T_Value_182 -> AgdaAny
forall a b. a -> b
coe T_Value_182
v10))))
T_Progress_514
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Progress_514
C_fail_528
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_constr'45'error_354)
T_Progress_514
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
[AgdaAny]
_ -> T_Progress_514
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v1 [T__'8866'_14]
v2
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v3
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> T_Progress_514
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_case'45'ƛ_422)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v3 T__'8866'_14
v4
-> let v5 :: T_Progress_514
v5 = T__'8866'_14 -> T_Progress_514
d_progress_532 (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v3) in
AgdaAny -> T_Progress_514
forall a b. a -> b
coe
(case T_Progress_514 -> T_Progress_514
forall a b. a -> b
coe T_Progress_514
v5 of
C_step_522 T__'8866'_14
v7 T__'10230'__256
v8
-> let v9 :: t
v9
= (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v7) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v4) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v10 :: t
v10 = (T__'10230'__256 -> T__'10230'__256) -> T__'10230'__256 -> t
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_ξ'8321'_266 T__'10230'__256
v8 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v10)))
C_done_526 T_Value_182
v7
-> let v8 :: T_Progress_514
v8 = T__'8866'_14 -> T_Progress_514
d_progress_532 (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v4) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case T_Progress_514 -> T_Progress_514
forall a b. a -> b
coe T_Progress_514
v8 of
C_step_522 T__'8866'_14
v10 T__'10230'__256
v11
-> let v12 :: t
v12
= (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v3)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v10) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v13 :: t
v13 = (T_Value_182 -> T__'10230'__256 -> T__'10230'__256)
-> T_Value_182 -> T__'10230'__256 -> t
forall a b. a -> b
coe T_Value_182 -> T__'10230'__256 -> T__'10230'__256
C_ξ'8322'_274 T_Value_182
v7 T__'10230'__256
v11 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v12) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v13)))
C_done_526 T_Value_182
v10
-> case T_Value_182 -> T_Value_182
forall a b. a -> b
coe T_Value_182
v7 of
T_Value_182
C_delay_188
-> let v12 :: b
v12 = T__'8866'_14 -> b
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v13 :: b
v13 = T__'10230'__256 -> b
forall a b. a -> b
coe T__'10230'__256
C_app'45'delay_404 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v12)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v13)))
T_Value_182
C_ƛ_192
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v3 of
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v12
-> let v13 :: t
v13
= (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.RenamingSubstitution.du__'91'_'93'_468
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v12) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v4) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v14 :: t
v14 = (T_Value_182 -> T__'10230'__256) -> T_Value_182 -> t
forall a b. a -> b
coe T_Value_182 -> T__'10230'__256
C_β_286 T_Value_182
v10 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v13) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v14)))
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Value_182
C_con_196
-> let v12 :: b
v12 = T__'8866'_14 -> b
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v13 :: b
v13 = T__'10230'__256 -> b
forall a b. a -> b
coe T__'10230'__256
C_app'45'con_398 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v12)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v13)))
T_Value_182
C_builtin_200
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v3 of
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v12
-> let v13 :: Integer
v13
= Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(((AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> Integer
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_216
(let v13 :: a -> Integer
v13
= \ a
v13 ->
Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer))
(a -> Integer
forall a b. a -> b
coe a
v13) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe ((AgdaAny -> AgdaAny -> Integer) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v14 -> AgdaAny -> Integer
forall {a}. a -> Integer
v13)))
(Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer))
((T_List'8314'_22 -> [AgdaAny]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_List'8314'_22 -> [AgdaAny]
MAlonzo.Code.Data.List.NonEmpty.Base.d_tail_32
((T_Sig_68 -> T_List'8314'_22) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Sig_68 -> T_List'8314'_22
MAlonzo.Code.Builtin.Signature.d_args_82
((T_Builtin_2 -> T_Sig_68) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Builtin_2 -> T_Sig_68
MAlonzo.Code.Builtin.d_signature_280
(T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v12))))) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v14 :: Integer
v14
= Integer -> Integer -> Integer
addInt
((T_Sig_68 -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe
T_Sig_68 -> Integer
MAlonzo.Code.Builtin.Signature.d_fv'9839'_80
((T_Builtin_2 -> T_Sig_68) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Builtin_2 -> T_Sig_68
MAlonzo.Code.Builtin.d_signature_280
(T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v12)))
((T_Sig_68 -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe
T_Sig_68 -> Integer
MAlonzo.Code.Builtin.Signature.d_fv'8902'_78
((T_Builtin_2 -> T_Sig_68) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Builtin_2 -> T_Sig_68
MAlonzo.Code.Builtin.d_signature_280
(T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v12))) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v14 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v13 of
Integer
1 -> let v15 :: t
v15
= AgdaAny -> AgdaAny -> T__'8866'_14 -> t
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased T__'8866'_14
v1 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v16 :: b
v16
= T__'10230'__256 -> b
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v15)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v16)))
Integer
_ -> let v15 :: Integer
v15
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v13)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
2 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> T__'10230'__256) -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> T__'10230'__256
C_case'45'unsat'8321'_458
Integer
v15))
Integer
_ -> let v15 :: Integer
v15
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v14)
(Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v16 :: b
v16
= T__'8866'_14 -> b
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v17 :: t
v17
= (Integer -> Integer -> T__'10230'__256) -> Integer -> Integer -> t
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392
Integer
v15 Integer
v13 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v16) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v17))))))
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
C_unsat'8320'_208 Integer
v12 Integer
v13 T_Value_182
v15
-> let v16 :: b
v16 = T__'8866'_14 -> b
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v17 :: t
v17
= (Integer -> Integer -> T__'10230'__256) -> Integer -> Integer -> t
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392 Integer
v12
Integer
v13 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v16)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v17)))
C_unsat'8320''8331''8321'_214 Integer
v12 T_Value_182
v14
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v3 of
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v15
-> let v16 :: t
v16 = (T__'8866'_14 -> T_Arity_4) -> AgdaAny -> t
forall a b. a -> b
coe T__'8866'_14 -> T_Arity_4
du_sat_36 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v15) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Arity_4
forall a b. a -> b
coe AgdaAny
forall a. a
v16 of
T_Arity_4
C_no'45'builtin_6
-> case AgdaAny -> T_Arity_4
forall a b. a -> b
coe AgdaAny
forall a. a
v16 of
T_Arity_4
C_no'45'builtin_6
-> let v17 :: t
v17
= ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> t
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
AgdaAny
forall a. a
erased in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Progress_514
forall a b. a -> b
coe AgdaAny
forall a. a
v17 of
C_step_522 T__'8866'_14
v19 T__'10230'__256
v20
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v19)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
T__'10230'__256
v20)
C_done_526 T_Value_182
v19
-> case T_Value_182 -> T_Value_182
forall a b. a -> b
coe T_Value_182
v19 of
C_unsat'8321'_222 Integer
v22 T_Value_182
v24 T_Value_182
v25
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> T__'10230'__256) -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> T__'10230'__256
C_case'45'unsat'8321'_458
Integer
v22)
T_Value_182
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Progress_514
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
C_want_8 Integer
v17 Integer
v18
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v17 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v18 of
Integer
0 -> let v19 :: t
v19
= (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v3)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
v4) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v20 :: t
v20
= (T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> t
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_ξ'8321'_266
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'force'45'builtin_310) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v19)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v20)))
Integer
1 -> let v19 :: t
v19
= AgdaAny -> AgdaAny -> T__'8866'_14 -> t
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v1 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v20 :: b
v20
= T__'10230'__256 -> b
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v19)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v20)))
Integer
_ -> let v19 :: Integer
v19
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe
Integer
v18)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
2 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> T__'10230'__256) -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> T__'10230'__256
C_case'45'unsat'8321'_458
Integer
v19))
Integer
_ -> let v19 :: Integer
v19
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v17)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
1 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v20 :: b
v20
= T__'8866'_14 -> b
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v21 :: t
v21
= (Integer -> Integer -> T__'10230'__256) -> Integer -> Integer -> t
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392
Integer
v19
Integer
v18 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v20)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v21))))
T_Arity_4
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
C_want_8 Integer
v17 Integer
v18
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v17 of
Integer
0 -> let v19 :: b
v19
= AgdaAny -> b -> b
forall a b. a -> b -> b
seq
(Integer -> AgdaAny
forall a b. a -> b
coe Integer
v18)
(AgdaAny -> AgdaAny -> b
forall a b. a -> b
coe
AgdaAny
forall a. a
d_interleave'45'error_32
AgdaAny
forall a. a
erased) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Arity_4
forall a b. a -> b
coe AgdaAny
forall a. a
v19 of
T_Arity_4
C_no'45'builtin_6
-> let v20 :: t
v20
= ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> t
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
AgdaAny
forall a. a
erased in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Progress_514
forall a b. a -> b
coe AgdaAny
forall a. a
v20 of
C_step_522 T__'8866'_14
v22 T__'10230'__256
v23
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
v22)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
T__'10230'__256
v23)
C_done_526 T_Value_182
v22
-> case T_Value_182 -> T_Value_182
forall a b. a -> b
coe
T_Value_182
v22 of
C_unsat'8321'_222 Integer
v25 T_Value_182
v27 T_Value_182
v28
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> T__'10230'__256) -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> T__'10230'__256
C_case'45'unsat'8321'_458
Integer
v25)
T_Value_182
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Progress_514
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
C_want_8 Integer
v20 Integer
v21
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v20 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe
Integer
v21 of
Integer
0 -> let v22 :: t
v22
= (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v3)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
v4) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v23 :: t
v23
= (T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> t
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_ξ'8321'_266
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'force'45'builtin_310) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v22)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v23)))
Integer
1 -> let v22 :: t
v22
= AgdaAny -> AgdaAny -> T__'8866'_14 -> t
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v1 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v23 :: b
v23
= T__'10230'__256 -> b
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v22)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v23)))
Integer
_ -> let v22 :: Integer
v22
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe
Integer
v21)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
2 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> T__'10230'__256) -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> T__'10230'__256
C_case'45'unsat'8321'_458
Integer
v22))
Integer
_ -> let v22 :: Integer
v22
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe
Integer
v20)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
1 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v23 :: b
v23
= T__'8866'_14 -> b
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v24 :: t
v24
= (Integer -> Integer -> T__'10230'__256) -> Integer -> Integer -> t
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392
Integer
v22
Integer
v21 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v23)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v24))))
T_Arity_4
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
Integer
1 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v18 of
Integer
0 -> let v19 :: t
v19
= (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased T__'8866'_14
v3)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v4) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v20 :: t
v20
= (T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> t
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_ξ'8321'_266
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'force'45'builtin_310) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v19)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v20)))
Integer
1 -> let v19 :: t
v19
= AgdaAny -> AgdaAny -> T__'8866'_14 -> t
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased T__'8866'_14
v1 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v20 :: b
v20
= T__'10230'__256 -> b
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v19)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v20)))
Integer
_ -> let v19 :: Integer
v19
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v18)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
2 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> T__'10230'__256) -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> T__'10230'__256
C_case'45'unsat'8321'_458
Integer
v19))
Integer
_ -> let v19 :: Integer
v19
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v17)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
2 :: Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v20 :: b
v20
= T__'8866'_14 -> b
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v21 :: t
v21
= (Integer -> Integer -> T__'10230'__256) -> Integer -> Integer -> t
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392
Integer
v19 Integer
v18 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v20)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v21))))
T_Arity_4
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
C_unsat'8321'_222 Integer
v13 T_Value_182
v15 T_Value_182
v16
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v3 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v17 T__'8866'_14
v18
-> let v19 :: t
v19 = (T__'8866'_14 -> T_Arity_4) -> AgdaAny -> t
forall a b. a -> b
coe T__'8866'_14 -> T_Arity_4
du_sat_36 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v17) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Arity_4
forall a b. a -> b
coe AgdaAny
forall a. a
v19 of
T_Arity_4
C_no'45'builtin_6
-> case AgdaAny -> T_Arity_4
forall a b. a -> b
coe AgdaAny
forall a. a
v19 of
T_Arity_4
C_no'45'builtin_6
-> let v20 :: t
v20
= ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> t
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
AgdaAny
forall a. a
erased in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Progress_514
forall a b. a -> b
coe AgdaAny
forall a. a
v20 of
C_step_522 T__'8866'_14
v22 T__'10230'__256
v23
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v22)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
T__'10230'__256
v23)
C_done_526 T_Value_182
v22
-> case T_Value_182 -> T_Value_182
forall a b. a -> b
coe T_Value_182
v22 of
C_unsat'8321'_222 Integer
v25 T_Value_182
v27 T_Value_182
v28
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> T__'10230'__256) -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> T__'10230'__256
C_case'45'unsat'8321'_458
Integer
v25)
T_Value_182
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Progress_514
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
C_want_8 Integer
v20 Integer
v21
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v20 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v21 of
Integer
0 -> let v22 :: t
v22
= (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v3)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
v4) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v23 :: t
v23
= (T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> t
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_ξ'8321'_266
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v22)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v23)))
Integer
1 -> let v22 :: t
v22
= AgdaAny -> AgdaAny -> T__'8866'_14 -> t
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v1 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v23 :: b
v23
= T__'10230'__256 -> b
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v22)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v23)))
Integer
_ -> let v22 :: Integer
v22
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe
Integer
v21)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
2 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> T__'10230'__256) -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> T__'10230'__256
C_case'45'unsat'8321'_458
Integer
v22))
Integer
_ -> let v22 :: Integer
v22
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v20)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
1 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v23 :: b
v23
= T__'8866'_14 -> b
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v24 :: t
v24
= (Integer -> Integer -> T__'10230'__256) -> Integer -> Integer -> t
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392
Integer
v22
Integer
v21 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v23)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v24))))
T_Arity_4
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
C_want_8 Integer
v20 Integer
v21
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v20 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v21 of
Integer
0 -> let v22 :: Integer
v22
= Integer
0 :: Integer in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v23 :: Integer
v23
= Integer
0 ::
Integer in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v22 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe
Integer
v23 of
Integer
0 -> let v24 :: t
v24
= (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v3)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
v4) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v25 :: t
v25
= (T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> t
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_ξ'8321'_266
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v24)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v25)))
Integer
1 -> let v24 :: t
v24
= AgdaAny -> AgdaAny -> T__'8866'_14 -> t
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v1 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v25 :: b
v25
= T__'10230'__256 -> b
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v24)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v25)))
Integer
_ -> let v24 :: Integer
v24
= -Integer
2 ::
Integer in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> T__'10230'__256) -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> T__'10230'__256
C_case'45'unsat'8321'_458
Integer
v24))
Integer
_ -> let v24 :: Integer
v24
= -Integer
1 ::
Integer in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v25 :: b
v25
= T__'8866'_14 -> b
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v26 :: t
v26
= (Integer -> Integer -> T__'10230'__256) -> Integer -> Integer -> t
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392
Integer
v24
Integer
v23 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v25)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v26))))))
Integer
_ -> let v22 :: Integer
v22
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v21)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
1 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v23 :: Integer
v23
= Integer
0 ::
Integer in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v23 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe
Integer
v21 of
Integer
1 -> let v24 :: t
v24
= (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v3)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
v4) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v25 :: t
v25
= (T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> t
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_ξ'8321'_266
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v24)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v25)))
Integer
2 -> let v24 :: t
v24
= AgdaAny -> AgdaAny -> T__'8866'_14 -> t
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v1 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v25 :: b
v25
= T__'10230'__256 -> b
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v24)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v25)))
Integer
_ -> let v24 :: Integer
v24
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe
Integer
v21)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
3 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> T__'10230'__256) -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> T__'10230'__256
C_case'45'unsat'8321'_458
Integer
v24))
Integer
_ -> let v24 :: Integer
v24
= -Integer
1 ::
Integer in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v25 :: b
v25
= T__'8866'_14 -> b
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v26 :: t
v26
= (Integer -> Integer -> T__'10230'__256) -> Integer -> Integer -> t
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392
Integer
v24
Integer
v22 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v25)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v26))))))
Integer
_ -> let v22 :: t
v22
= AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
AgdaAny
forall a. a
d_interleave'45'error_32
AgdaAny
forall a. a
erased in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Arity_4
forall a b. a -> b
coe AgdaAny
forall a. a
v22 of
T_Arity_4
C_no'45'builtin_6
-> let v23 :: t
v23
= ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> t
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
AgdaAny
forall a. a
erased in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Progress_514
forall a b. a -> b
coe AgdaAny
forall a. a
v23 of
C_step_522 T__'8866'_14
v25 T__'10230'__256
v26
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
v25)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
T__'10230'__256
v26)
C_done_526 T_Value_182
v25
-> case T_Value_182 -> T_Value_182
forall a b. a -> b
coe
T_Value_182
v25 of
C_unsat'8321'_222 Integer
v28 T_Value_182
v30 T_Value_182
v31
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> T__'10230'__256) -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> T__'10230'__256
C_case'45'unsat'8321'_458
Integer
v28)
T_Value_182
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Progress_514
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
C_want_8 Integer
v23 Integer
v24
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v23 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe
Integer
v24 of
Integer
0 -> let v25 :: t
v25
= (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
(AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v3)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
v4) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v26 :: t
v26
= (T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> t
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_ξ'8321'_266
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v25)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v26)))
Integer
1 -> let v25 :: t
v25
= AgdaAny -> AgdaAny -> T__'8866'_14 -> t
forall a b. a -> b
coe
AgdaAny
forall a. a
d_reduceBuiltin_252
AgdaAny
forall a. a
erased
T__'8866'_14
v1 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v26 :: b
v26
= T__'10230'__256 -> b
forall a b. a -> b
coe
T__'10230'__256
C_sat'45'app'45'builtin_306 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v25)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v26)))
Integer
_ -> let v25 :: Integer
v25
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe
Integer
v24)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
2 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> T__'10230'__256) -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> T__'10230'__256
C_case'45'unsat'8321'_458
Integer
v25))
Integer
_ -> let v25 :: Integer
v25
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe
Integer
v23)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
1 ::
Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v26 :: b
v26
= T__'8866'_14 -> b
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v27 :: t
v27
= (Integer -> Integer -> T__'10230'__256) -> Integer -> Integer -> t
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_app'45'interleave'45'error_392
Integer
v25
Integer
v24 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v26)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
[T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466
AgdaAny
forall a. a
v27))))
T_Arity_4
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Arity_4
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
C_constr_228 T_All_44
v13
-> let v14 :: b
v14 = T__'8866'_14 -> b
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v15 :: b
v15 = T__'10230'__256 -> b
forall a b. a -> b
coe T__'10230'__256
C_app'45'constr_412 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v14)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v15)))
T_Value_182
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Progress_514
C_fail_528
-> let v9 :: b
v9 = T__'8866'_14 -> b
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v10 :: b
v10 = T__'10230'__256 -> b
forall a b. a -> b
coe T__'10230'__256
C_error'8322'_298 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v10)))
T_Progress_514
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Progress_514
C_fail_528
-> let v6 :: b
v6 = T__'8866'_14 -> b
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v7 :: b
v7 = T__'10230'__256 -> b
forall a b. a -> b
coe T__'10230'__256
C_error'8321'_294 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v6) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v7)))
T_Progress_514
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v3
-> let v4 :: T_Progress_514
v4 = T__'8866'_14 -> T_Progress_514
d_progress_532 (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v3) in
AgdaAny -> T_Progress_514
forall a b. a -> b
coe
(case T_Progress_514 -> T_Progress_514
forall a b. a -> b
coe T_Progress_514
v4 of
C_step_522 T__'8866'_14
v6 T__'10230'__256
v7
-> let v8 :: t
v8 = (T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> t
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_force_24 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v6) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v9 :: t
v9 = (T__'10230'__256 -> T__'10230'__256) -> T__'10230'__256 -> t
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_ξ'8323'_280 T__'10230'__256
v7 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v9)))
C_done_526 T_Value_182
v6
-> let v7 :: t
v7 = (T__'8866'_14 -> T_Arity_4) -> AgdaAny -> t
forall a b. a -> b
coe T__'8866'_14 -> T_Arity_4
du_sat_36 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v3) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Arity_4
forall a b. a -> b
coe AgdaAny
forall a. a
v7 of
T_Arity_4
C_no'45'builtin_6
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v3 of
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v8
-> let v9 :: b
v9 = T__'8866'_14 -> b
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v10 :: b
v10 = T__'10230'__256 -> b
forall a b. a -> b
coe T__'10230'__256
C_force'45'ƛ_366 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v10)))
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v8 T__'8866'_14
v9
-> let v10 :: b
v10
= AgdaAny -> b -> b
forall a b. a -> b -> b
seq
(T_Value_182 -> AgdaAny
forall a b. a -> b
coe T_Value_182
v6)
(((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> b
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
AgdaAny
forall a. a
erased) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Progress_514
forall a b. a -> b
coe AgdaAny
forall a. a
v10 of
C_step_522 T__'8866'_14
v12 T__'10230'__256
v13
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v12)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 T__'10230'__256
v13)
C_done_526 T_Value_182
v12
-> case T_Value_182 -> T_Value_182
forall a b. a -> b
coe T_Value_182
v12 of
C_unsat'8320'_208 Integer
v14 Integer
v15 T_Value_182
v17
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> Integer -> T__'10230'__256)
-> Integer -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_case'45'unsat'8320'_450 Integer
v14
Integer
v15)
C_unsat'8320''8331''8321'_214 Integer
v14 T_Value_182
v16
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> T__'10230'__256) -> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> T__'10230'__256
C_case'45'unsat'8321'_458 Integer
v14)
T_Value_182
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Progress_514
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v8
-> let v9 :: b
v9
= AgdaAny -> b -> b
forall a b. a -> b -> b
seq
(T_Value_182 -> AgdaAny
forall a b. a -> b
coe T_Value_182
v6)
(((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> b
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
AgdaAny
forall a. a
erased) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Progress_514
forall a b. a -> b
coe AgdaAny
forall a. a
v9 of
C_step_522 T__'8866'_14
v11 T__'10230'__256
v12
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v11)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 T__'10230'__256
v12)
C_done_526 T_Value_182
v11
-> case T_Value_182 -> T_Value_182
forall a b. a -> b
coe T_Value_182
v11 of
C_unsat'8320'_208 Integer
v13 Integer
v14 T_Value_182
v16
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> Integer -> T__'10230'__256)
-> Integer -> Integer -> AgdaAny
forall a b. a -> b
coe
Integer -> Integer -> T__'10230'__256
C_case'45'unsat'8320'_450 Integer
v13
Integer
v14)
C_unsat'8320''8331''8321'_214 Integer
v13 T_Value_182
v15
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> T__'10230'__256) -> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> T__'10230'__256
C_case'45'unsat'8321'_458 Integer
v13)
T_Value_182
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Progress_514
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v8
-> let v9 :: b
v9 = T__'10230'__256 -> b
forall a b. a -> b
coe T__'10230'__256
C_force'45'delay_290 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v8)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v9))
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v8
-> let v9 :: b
v9 = T__'8866'_14 -> b
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v10 :: b
v10 = T__'10230'__256 -> b
forall a b. a -> b
coe T__'10230'__256
C_force'45'con_370 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v10)))
MAlonzo.Code.Untyped.C_constr_34 Integer
v8 [T__'8866'_14]
v9
-> let v10 :: b
v10 = T__'8866'_14 -> b
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v11 :: b
v11 = T__'10230'__256 -> b
forall a b. a -> b
coe T__'10230'__256
C_force'45'constr_376 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v10)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v11)))
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> let v8 :: b
v8 = T__'10230'__256 -> b
forall a b. a -> b
coe T__'10230'__256
C_force'45'error_300 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v3)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v8))
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
C_want_8 Integer
v8 Integer
v9
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v8 of
Integer
0 -> let v10 :: b
v10 = T__'8866'_14 -> b
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v11 :: t
v11
= (Integer -> T__'10230'__256) -> Integer -> t
forall a b. a -> b
coe Integer -> T__'10230'__256
C_force'45'interleave'45'error_382 Integer
v9 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v10)
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v11)))
Integer
1 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v9 of
Integer
0 -> let v10 :: t
v10 = AgdaAny -> AgdaAny -> T__'8866'_14 -> t
forall a b. a -> b
coe AgdaAny
forall a. a
d_reduceBuiltin_252 AgdaAny
forall a. a
erased T__'8866'_14
v1 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v11 :: b
v11
= T__'10230'__256 -> b
forall a b. a -> b
coe T__'10230'__256
C_sat'45'force'45'builtin_310 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v10) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v11)))
Integer
_ -> let v10 :: Integer
v10
= Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v9) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> T__'10230'__256) -> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> T__'10230'__256
C_case'45'unsat'8321'_458 Integer
v10))
Integer
_ -> let v10 :: Integer
v10 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v8) (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
((Integer -> Integer -> T__'10230'__256)
-> Integer -> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> T__'10230'__256
C_case'45'unsat'8320'_450 Integer
v10 Integer
v9))
T_Arity_4
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Progress_514
C_fail_528
-> let v5 :: b
v5 = T__'8866'_14 -> b
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v6 :: b
v6 = T__'10230'__256 -> b
forall a b. a -> b
coe T__'10230'__256
C_force'45'error_300 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 AgdaAny
forall a. a
v6)))
T_Progress_514
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v3
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> T_Progress_514
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_case'45'delay_428)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v3
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> T_Progress_514
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_case'45'con_434)
MAlonzo.Code.Untyped.C_constr_34 Integer
v3 [T__'8866'_14]
v4
-> let v5 :: t
v5
= (Integer -> [AgdaAny] -> Maybe AgdaAny) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
Integer -> [AgdaAny] -> Maybe AgdaAny
MAlonzo.Code.Untyped.CEK.du_lookup'63'_954 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2) in
AgdaAny -> T_Progress_514
forall a b. a -> b
coe
(case AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v6
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 ((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
du_iterApp_242 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v4))
((T__'8866'_14 -> T__'10230'__256) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> T__'10230'__256
C_case'45'constr_320 AgdaAny
v6)
Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_broken'45'const_328)
Maybe AgdaAny
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v3 [T__'8866'_14]
v4
-> let v5 :: T_Progress_514
v5 = T__'8866'_14 -> T_Progress_514
d_progress_532 (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1) in
AgdaAny -> T_Progress_514
forall a b. a -> b
coe
(case T_Progress_514 -> T_Progress_514
forall a b. a -> b
coe T_Progress_514
v5 of
C_step_522 T__'8866'_14
v7 T__'10230'__256
v8
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 ((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v7) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v2))
((T__'10230'__256 -> T__'10230'__256) -> T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256 -> T__'10230'__256
C_case'45'reduce_466 T__'10230'__256
v8)
T_Progress_514
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v3
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> AgdaAny -> AgdaAny -> T_Progress_514
forall a b. a -> b
coe
T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
(T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_case'45'builtin_440)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (T__'8866'_14 -> T__'10230'__256 -> T_Progress_514)
-> T__'8866'_14 -> AgdaAny -> T_Progress_514
forall a b. a -> b
coe T__'8866'_14 -> T__'10230'__256 -> T_Progress_514
C_step_522 T__'8866'_14
v1 (T__'10230'__256 -> AgdaAny
forall a b. a -> b
coe T__'10230'__256
C_case'45'error_416)
T__'8866'_14
_ -> T_Progress_514
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v1
-> (T_Value_182 -> T_Progress_514) -> AgdaAny -> T_Progress_514
forall a b. a -> b
coe T_Value_182 -> T_Progress_514
C_done_526 (T_Value_182 -> AgdaAny
forall a b. a -> b
coe T_Value_182
C_builtin_200)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 -> T_Progress_514 -> T_Progress_514
forall a b. a -> b
coe T_Progress_514
C_fail_528
T__'8866'_14
_ -> T_Progress_514
forall a. a
MAlonzo.RTE.mazUnreachableError
d__'8773'__1202 :: p -> p -> p -> ()
d__'8773'__1202 p
a0 p
a1 p
a2 = ()
data T__'8773'__1202
= C_reduce_1212 MAlonzo.Code.Untyped.T__'8866'_14
T__'10230''42'__470 T__'10230''42'__470
d_refl'45''8773'_1218 ::
MAlonzo.Code.Untyped.T__'8866'_14 -> T__'8773'__1202
d_refl'45''8773'_1218 :: T__'8866'_14 -> T__'8773'__1202
d_refl'45''8773'_1218 T__'8866'_14
v0
= (T__'8866'_14
-> T__'10230''42'__470 -> T__'10230''42'__470 -> T__'8773'__1202)
-> T__'8866'_14 -> AgdaAny -> AgdaAny -> T__'8773'__1202
forall a b. a -> b
coe T__'8866'_14
-> T__'10230''42'__470 -> T__'10230''42'__470 -> T__'8773'__1202
C_reduce_1212 T__'8866'_14
v0 (T__'10230''42'__470 -> AgdaAny
forall a b. a -> b
coe T__'10230''42'__470
C_refl_476) (T__'10230''42'__470 -> AgdaAny
forall a b. a -> b
coe T__'10230''42'__470
C_refl_476)
d_integer_1220 :: MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4
d_integer_1220 :: T__'8866''9839'_4
d_integer_1220
= (T_Tag_28 AgdaAny -> T__'8866''9839'_4)
-> AgdaAny -> T__'8866''9839'_4
forall a b. a -> b
coe
T_Tag_28 AgdaAny -> T__'8866''9839'_4
MAlonzo.Code.RawU.du_tag2TyTag_206
(DefaultUni (Esc Integer) -> AgdaAny
forall a b. a -> b
coe DefaultUni (Esc Integer)
forall {a}. (a ~ Esc Integer) => DefaultUni a
MAlonzo.Code.RawU.C_integer_30)
d_con'45'integer_1224 ::
() -> Integer -> MAlonzo.Code.Untyped.T__'8866'_14
d_con'45'integer_1224 :: () -> Integer -> T__'8866'_14
d_con'45'integer_1224 ~()
v0 Integer
v1 = Integer -> T__'8866'_14
du_con'45'integer_1224 Integer
v1
du_con'45'integer_1224 ::
Integer -> MAlonzo.Code.Untyped.T__'8866'_14
du_con'45'integer_1224 :: Integer -> T__'8866'_14
du_con'45'integer_1224 Integer
v0
= (T_TmCon_198 -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T_TmCon_198 -> T__'8866'_14
MAlonzo.Code.Untyped.C_con_28
((T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198
MAlonzo.Code.RawU.C_tmCon_202 (T__'8866''9839'_4 -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4
d_integer_1220) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0))
d_ex1_1236 :: MAlonzo.Code.Untyped.T__'8866'_14
d_ex1_1236 :: T__'8866'_14
d_ex1_1236
= (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((AgdaAny -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
(Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))))
((AgdaAny -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
(Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))))
((AgdaAny -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
(Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)))))
((Integer -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_1224 (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
2 :: Integer))))
((Integer -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_1224 (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
3 :: Integer)))
d_ex2_1238 :: MAlonzo.Code.Untyped.T__'8866'_14
d_ex2_1238 :: T__'8866'_14
d_ex2_1238
= (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((AgdaAny -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
(Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))))
((AgdaAny -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
(Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))))
((AgdaAny -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
(Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)))))
((Integer -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_1224 (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
3 :: Integer))))
((Integer -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_1224 (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
2 :: Integer)))