{-# 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.Induction.WellFounded where
import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Induction
d_WfRec_22 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) -> AgdaAny -> ()
d_WfRec_22 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Level_18
d_WfRec_22 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Level_18
forall a. a
erased
d_Acc_42 :: p -> p -> p -> p -> p -> T_Level_18
d_Acc_42 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
data T_Acc_42 = C_acc_52
d_WellFounded_54 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) -> ()
d_WellFounded_54 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
d_WellFounded_54 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
forall a. a
erased
d_acc'45'inverse_66 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny -> T_Acc_42 -> AgdaAny -> AgdaAny -> T_Acc_42
d_acc'45'inverse_66 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> AgdaAny
-> T_Acc_42
d_acc'45'inverse_66 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> AgdaAny
-> T_Acc_42
forall a. a
erased
d_Acc'45'resp'45'flip'45''8776'_86 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> T_Acc_42 -> T_Acc_42
d_Acc'45'resp'45'flip'45''8776'_86 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
d_Acc'45'resp'45'flip'45''8776'_86 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
forall a. a
erased
d_Acc'45'resp'45''8776'_96 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> T_Acc_42 -> T_Acc_42
d_Acc'45'resp'45''8776'_96 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
d_Acc'45'resp'45''8776'_96 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
forall a. a
erased
d_wfRecBuilder_116 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
AgdaAny -> T_Acc_42 -> AgdaAny -> AgdaAny -> AgdaAny
d_wfRecBuilder_116 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_wfRecBuilder_116 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v6 ~AgdaAny
v7 ~T_Acc_42
v8 AgdaAny
v9 ~AgdaAny
v10
= (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny
du_wfRecBuilder_116 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v6 AgdaAny
v9
du_wfRecBuilder_116 ::
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
AgdaAny -> AgdaAny
du_wfRecBuilder_116 :: (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny
du_wfRecBuilder_116 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v0 AgdaAny
v1
= (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v0 AgdaAny
v1 (\ AgdaAny
v2 AgdaAny
v3 -> ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny
du_wfRecBuilder_116 ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v0) AgdaAny
v2)
d_wfRec_128 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
AgdaAny -> T_Acc_42 -> AgdaAny
d_wfRec_128 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
d_wfRec_128 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 = (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
du_wfRec_128
du_wfRec_128 ::
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
AgdaAny -> T_Acc_42 -> AgdaAny
du_wfRec_128 :: (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
du_wfRec_128
= (((AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> (AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
forall a b. a -> b
coe
((AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Induction.du_subsetBuild_62
(\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 -> ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny
du_wfRecBuilder_116 AgdaAny
v1 AgdaAny
v4)
d_unfold'45'wfRec_140 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
AgdaAny ->
T_Acc_42 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_unfold'45'wfRec_140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> T__'8801'__12
d_unfold'45'wfRec_140 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> T__'8801'__12
forall a. a
erased
d_wfRecBuilder_160 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> T_Acc_42) ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_wfRecBuilder_160 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_wfRecBuilder_160 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> T_Acc_42
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v7 ~AgdaAny
v8 AgdaAny
v9
= (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
du_wfRecBuilder_160 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v7 AgdaAny
v9
du_wfRecBuilder_160 ::
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny
du_wfRecBuilder_160 :: (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
du_wfRecBuilder_160 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2
= ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny
du_wfRecBuilder_116 ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
d_wfRec_168 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> T_Acc_42) ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
AgdaAny -> AgdaAny
d_wfRec_168 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_wfRec_168 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> T_Acc_42
v4 ~T_Level_18
v5 = (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_wfRec_168
du_wfRec_168 ::
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
AgdaAny -> AgdaAny
du_wfRec_168 :: (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_wfRec_168
= (((AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
((AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Induction.du_build_36
(\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
du_wfRecBuilder_160 AgdaAny
v1 AgdaAny
v3)
d_wfRec'45'builder_170 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> T_Acc_42) ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_wfRec'45'builder_170 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_wfRec'45'builder_170 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> T_Acc_42
v4 ~T_Level_18
v5
= (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_wfRec'45'builder_170
du_wfRec'45'builder_170 ::
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_wfRec'45'builder_170 :: (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_wfRec'45'builder_170 AgdaAny -> T_Level_18
v0 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 = ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
du_wfRecBuilder_160 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v1 AgdaAny
v3
d_some'45'wfrec'45'Irrelevant_200 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> T_Acc_42) ->
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
(AgdaAny ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
AgdaAny -> ()
d_some'45'wfrec'45'Irrelevant_200 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T__'8801'__12)
-> AgdaAny
-> T_Level_18
d_some'45'wfrec'45'Irrelevant_200 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T__'8801'__12)
-> AgdaAny
-> T_Level_18
forall a. a
erased
d_some'45'wfRec'45'irrelevant_210 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> T_Acc_42) ->
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
(AgdaAny ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
AgdaAny ->
T_Acc_42 ->
T_Acc_42 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_some'45'wfRec'45'irrelevant_210 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T__'8801'__12)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
-> T__'8801'__12
d_some'45'wfRec'45'irrelevant_210 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T__'8801'__12)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
-> T__'8801'__12
forall a. a
erased
d_wfRec_226 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> T_Acc_42) ->
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
(AgdaAny ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
AgdaAny -> AgdaAny
d_wfRec_226 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T__'8801'__12)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_wfRec_226 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Acc_42
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v7 ~AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v8 = (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_wfRec_226
du_wfRec_226 ::
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
AgdaAny -> AgdaAny
du_wfRec_226 :: (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_wfRec_226 = ((AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_wfRec_168
d_wfRec'45'builder_228 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> T_Acc_42) ->
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
(AgdaAny ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_wfRec'45'builder_228 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T__'8801'__12)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_wfRec'45'builder_228 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Acc_42
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v7 ~AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v8
= (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_wfRec'45'builder_228
du_wfRec'45'builder_228 ::
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_wfRec'45'builder_228 :: (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_wfRec'45'builder_228 = ((AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_wfRec'45'builder_170
d_wfRecBuilder_230 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> T_Acc_42) ->
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
(AgdaAny ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_wfRecBuilder_230 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T__'8801'__12)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_wfRecBuilder_230 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Acc_42
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v7 ~AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T__'8801'__12
v8
= (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_wfRecBuilder_230
du_wfRecBuilder_230 ::
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_wfRecBuilder_230 :: (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_wfRecBuilder_230 AgdaAny -> T_Level_18
v0 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 = ((AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
du_wfRecBuilder_160 AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
v1 AgdaAny
v3
d_wfRecBuilder'45'wfRec_238 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> T_Acc_42) ->
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
(AgdaAny ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
AgdaAny ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_wfRecBuilder'45'wfRec_238 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T__'8801'__12)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
d_wfRecBuilder'45'wfRec_238 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T__'8801'__12)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
d_unfold'45'wfRec_256 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> T_Acc_42) ->
(AgdaAny -> ()) ->
(AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) ->
(AgdaAny ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_unfold'45'wfRec_256 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T__'8801'__12)
-> AgdaAny
-> T__'8801'__12
d_unfold'45'wfRec_256 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny)
-> (AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8801'__12)
-> T__'8801'__12)
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
d_acc'8658'asym_274 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny ->
AgdaAny ->
T_Acc_42 ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_acc'8658'asym_274 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
d_acc'8658'asym_274 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
d_wf'8658'asym_292 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> T_Acc_42) ->
AgdaAny ->
AgdaAny ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_wf'8658'asym_292 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
d_wf'8658'asym_292 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
d_wf'8658'irrefl_298 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> T_Acc_42) ->
AgdaAny ->
AgdaAny ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_wf'8658'irrefl_298 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
d_wf'8658'irrefl_298 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
d_accessible_324 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> T_Acc_42 -> T_Acc_42
d_accessible_324 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
d_accessible_324 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
forall a. a
erased
d_wellFounded_330 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42
d_wellFounded_330 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
d_wellFounded_330 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
forall a. a
erased
d_accessible_350 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) -> AgdaAny -> T_Acc_42 -> T_Acc_42
d_accessible_350 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
d_accessible_350 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
forall a. a
erased
d_wellFounded_356 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42
d_wellFounded_356 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
d_wellFounded_356 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
forall a. a
erased
d_well'45'founded_362 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42
d_well'45'founded_362 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
d_well'45'founded_362 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
forall a. a
erased
d__'60''8314'__374 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'60''8314'__374 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T__'60''8314'__374
= C_'91'_'93'_382 AgdaAny |
C_trans_394 AgdaAny T__'60''8314'__374 T__'60''8314'__374
d_downwardsClosed_400 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny -> AgdaAny -> T_Acc_42 -> T__'60''8314'__374 -> T_Acc_42
d_downwardsClosed_400 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T__'60''8314'__374
-> T_Acc_42
d_downwardsClosed_400 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T__'60''8314'__374
-> T_Acc_42
forall a. a
erased
d_accessible_410 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> T_Acc_42 -> T_Acc_42
d_accessible_410 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
d_accessible_410 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
forall a. a
erased
d_accessible'8242'_414 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny -> T_Acc_42 -> AgdaAny -> T__'60''8314'__374 -> T_Acc_42
d_accessible'8242'_414 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> T__'60''8314'__374
-> T_Acc_42
d_accessible'8242'_414 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> T__'60''8314'__374
-> T_Acc_42
forall a. a
erased
d_wellFounded_428 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42
d_wellFounded_428 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
d_wellFounded_428 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
forall a. a
erased
d__'60'__454 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> T_Level_18
d__'60'__454 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 p
a9 = ()
data T__'60'__454 = C_left_466 AgdaAny | C_right_476 AgdaAny
d_accessible_484 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> ()) ->
AgdaAny ->
AgdaAny -> T_Acc_42 -> (AgdaAny -> AgdaAny -> T_Acc_42) -> T_Acc_42
d_accessible_484 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> (AgdaAny -> AgdaAny -> T_Acc_42)
-> T_Acc_42
d_accessible_484 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> (AgdaAny -> AgdaAny -> T_Acc_42)
-> T_Acc_42
forall a. a
erased
d_accessible'8242'_492 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> ()) ->
AgdaAny ->
AgdaAny ->
T_Acc_42 ->
T_Acc_42 ->
(AgdaAny -> AgdaAny -> T_Acc_42) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T__'60'__454 -> T_Acc_42
d_accessible'8242'_492 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
-> (AgdaAny -> AgdaAny -> T_Acc_42)
-> T_Σ_14
-> T__'60'__454
-> T_Acc_42
d_accessible'8242'_492 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
-> (AgdaAny -> AgdaAny -> T_Acc_42)
-> T_Σ_14
-> T__'60'__454
-> T_Acc_42
forall a. a
erased
d_wellFounded_514 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> T_Acc_42) ->
(AgdaAny -> AgdaAny -> T_Acc_42) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Acc_42
d_wellFounded_514 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> AgdaAny -> T_Acc_42)
-> T_Σ_14
-> T_Acc_42
d_wellFounded_514 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> AgdaAny -> T_Acc_42)
-> T_Σ_14
-> T_Acc_42
forall a. a
erased
d_well'45'founded_522 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> T_Acc_42) ->
(AgdaAny -> AgdaAny -> T_Acc_42) ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Acc_42
d_well'45'founded_522 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> AgdaAny -> T_Acc_42)
-> T_Σ_14
-> T_Acc_42
d_well'45'founded_522 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> (AgdaAny -> AgdaAny -> T_Acc_42)
-> T_Σ_14
-> T_Acc_42
forall a. a
erased
d_accessible_526 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) -> AgdaAny -> T_Acc_42 -> T_Acc_42
d_accessible_526 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
d_accessible_526 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
forall a. a
erased
d_well'45'founded_528 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42
d_well'45'founded_528 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
d_well'45'founded_528 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
forall a. a
erased
d_wellFounded_530 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42
d_wellFounded_530 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
d_wellFounded_530 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
forall a. a
erased
d__'60''8314'__534 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'60''8314'__534 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
d_accessible_538 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> T_Acc_42 -> T_Acc_42
d_accessible_538 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
d_accessible_538 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> T_Acc_42
forall a. a
erased
d_accessible'8242'_540 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny -> T_Acc_42 -> AgdaAny -> T__'60''8314'__374 -> T_Acc_42
d_accessible'8242'_540 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> T__'60''8314'__374
-> T_Acc_42
d_accessible'8242'_540 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> T_Acc_42
-> AgdaAny
-> T__'60''8314'__374
-> T_Acc_42
forall a. a
erased
d_downwardsClosed_542 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
AgdaAny -> AgdaAny -> T_Acc_42 -> T__'60''8314'__374 -> T_Acc_42
d_downwardsClosed_542 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T__'60''8314'__374
-> T_Acc_42
d_downwardsClosed_542 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Acc_42
-> T__'60''8314'__374
-> T_Acc_42
forall a. a
erased
d_wellFounded_546 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42
d_wellFounded_546 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
d_wellFounded_546 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Acc_42)
-> AgdaAny
-> T_Acc_42
forall a. a
erased
d_'46'generalizedField'45'A'46'a_6161 ::
T_GeneralizeTel_6167 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'A'46'a_6161 :: T_GeneralizeTel_6167 -> T_Level_18
d_'46'generalizedField'45'A'46'a_6161 T_GeneralizeTel_6167
v0
= case T_GeneralizeTel_6167 -> T_GeneralizeTel_6167
forall a b. a -> b
coe T_GeneralizeTel_6167
v0 of
C_mkGeneralizeTel_6169 T_Level_18
v1 T_Level_18
v3 -> T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
v1
T_GeneralizeTel_6167
_ -> T_Level_18
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'46'generalizedField'45'A_6163 :: T_GeneralizeTel_6167 -> ()
d_'46'generalizedField'45'A_6163 :: T_GeneralizeTel_6167 -> T_Level_18
d_'46'generalizedField'45'A_6163 = T_GeneralizeTel_6167 -> T_Level_18
forall a. a
erased
d_'46'generalizedField'45'r_6165 ::
T_GeneralizeTel_6167 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'r_6165 :: T_GeneralizeTel_6167 -> T_Level_18
d_'46'generalizedField'45'r_6165 T_GeneralizeTel_6167
v0
= case T_GeneralizeTel_6167 -> T_GeneralizeTel_6167
forall a b. a -> b
coe T_GeneralizeTel_6167
v0 of
C_mkGeneralizeTel_6169 T_Level_18
v1 T_Level_18
v3 -> T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
v3
T_GeneralizeTel_6167
_ -> T_Level_18
forall a. a
MAlonzo.RTE.mazUnreachableError
d_GeneralizeTel_6167 :: T_Level_18
d_GeneralizeTel_6167 = ()
data T_GeneralizeTel_6167
= C_mkGeneralizeTel_6169 MAlonzo.Code.Agda.Primitive.T_Level_18
MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'A'46'a_10101 ::
T_GeneralizeTel_10107 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'A'46'a_10101 :: T_GeneralizeTel_10107 -> T_Level_18
d_'46'generalizedField'45'A'46'a_10101 T_GeneralizeTel_10107
v0
= case T_GeneralizeTel_10107 -> T_GeneralizeTel_10107
forall a b. a -> b
coe T_GeneralizeTel_10107
v0 of
C_mkGeneralizeTel_10109 T_Level_18
v1 T_Level_18
v3 -> T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
v1
T_GeneralizeTel_10107
_ -> T_Level_18
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'46'generalizedField'45'A_10103 :: T_GeneralizeTel_10107 -> ()
d_'46'generalizedField'45'A_10103 :: T_GeneralizeTel_10107 -> T_Level_18
d_'46'generalizedField'45'A_10103 = T_GeneralizeTel_10107 -> T_Level_18
forall a. a
erased
d_'46'generalizedField'45'r_10105 ::
T_GeneralizeTel_10107 -> MAlonzo.Code.Agda.Primitive.T_Level_18
d_'46'generalizedField'45'r_10105 :: T_GeneralizeTel_10107 -> T_Level_18
d_'46'generalizedField'45'r_10105 T_GeneralizeTel_10107
v0
= case T_GeneralizeTel_10107 -> T_GeneralizeTel_10107
forall a b. a -> b
coe T_GeneralizeTel_10107
v0 of
C_mkGeneralizeTel_10109 T_Level_18
v1 T_Level_18
v3 -> T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
v3
T_GeneralizeTel_10107
_ -> T_Level_18
forall a. a
MAlonzo.RTE.mazUnreachableError
d_GeneralizeTel_10107 :: T_Level_18
d_GeneralizeTel_10107 = ()
data T_GeneralizeTel_10107
= C_mkGeneralizeTel_10109 MAlonzo.Code.Agda.Primitive.T_Level_18
MAlonzo.Code.Agda.Primitive.T_Level_18