Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Induction.WellFounded

Documentation

d_WfRec_22 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → AgdaAny → () Source #

d_Acc_42 ∷ p → p → p → p → p → () Source #

data T_Acc_42 Source #

Constructors

C_acc_52

d_WellFounded_54 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #

d_acc'45'inverse_66 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → T_Acc_42 → AgdaAny → AgdaAny → T_Acc_42 Source #

d_Acc'45'resp'45'flip'45''8776'_86 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_Acc_42 → T_Acc_42 Source #

d_Acc'45'resp'45''8776'_96 ∷ T_Level_18 → () → T_Level_18 → 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 Source #

d_wfRecBuilder_116 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → T_Acc_42 → AgdaAny → AgdaAny → AgdaAny Source #

du_wfRecBuilder_116 ∷ (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny Source #

d_wfRec_128 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → T_Acc_42 → AgdaAny Source #

du_wfRec_128 ∷ (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → T_Acc_42 → AgdaAny Source #

d_unfold'45'wfRec_140 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → T_Acc_42 → T__'8801'__12 Source #

d_wfRecBuilder_160 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_wfRecBuilder_160 ∷ (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #

d_wfRec_168 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny Source #

du_wfRec_168 ∷ (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny Source #

d_wfRec'45'builder_170 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_wfRec'45'builder_170 ∷ (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_some'45'wfrec'45'Irrelevant_200 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12) → T__'8801'__12) → AgdaAny → () Source #

d_some'45'wfRec'45'irrelevant_210 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → (AgdaAny → ()) → (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 Source #

d_wfRec_226 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12) → T__'8801'__12) → (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny Source #

du_wfRec_226 ∷ (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny Source #

d_wfRec'45'builder_228 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12) → T__'8801'__12) → (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_wfRec'45'builder_228 ∷ (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_wfRecBuilder_230 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12) → T__'8801'__12) → (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_wfRecBuilder_230 ∷ (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_wfRecBuilder'45'wfRec_238 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → (AgdaAny → ()) → (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 Source #

d_unfold'45'wfRec_256 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12) → T__'8801'__12) → AgdaAny → T__'8801'__12 Source #

d_acc'8658'asym_274 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Acc_42 → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_wf'8658'asym_292 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_wf'8658'irrefl_298 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → T_Acc_42) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_accessible_324 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Acc_42 → T_Acc_42 Source #

d_wellFounded_330 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → T_Acc_42) → AgdaAny → T_Acc_42 Source #

d_accessible_350 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → T_Acc_42 → T_Acc_42 Source #

d_wellFounded_356 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → T_Acc_42) → AgdaAny → T_Acc_42 Source #

d_well'45'founded_362 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → T_Acc_42) → AgdaAny → T_Acc_42 Source #

d__'60''8314'__374 ∷ p → p → p → p → p → p → () Source #

data T__'60''8314'__374 Source #

Constructors

C_'91'_'93'_382 AgdaAny
C_trans_394 AgdaAny T__'60''8314'__374 T__'60''8314'__374

d_downwardsClosed_400 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Acc_42 → T__'60''8314'__374 → T_Acc_42 Source #

d_accessible_410 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → T_Acc_42 → T_Acc_42 Source #

d_accessible'8242'_414 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → T_Acc_42 → AgdaAny → T__'60''8314'__374 → T_Acc_42 Source #

d_wellFounded_428 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → AgdaAny → T_Acc_42 Source #

d__'60'__454 ∷ p → p → p → p → p → p → p → p → p → p → () Source #

data T__'60'__454 Source #

Constructors

C_left_466 AgdaAny
C_right_476 AgdaAny

d_accessible_484 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Acc_42 → (AgdaAny → AgdaAny → T_Acc_42) → T_Acc_42 Source #

d_accessible'8242'_492 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Acc_42 → T_Acc_42 → (AgdaAny → AgdaAny → T_Acc_42) → T_Σ_14 → T__'60'__454 → T_Acc_42 Source #

d_wellFounded_514 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → (AgdaAny → AgdaAny → T_Acc_42) → T_Σ_14 → T_Acc_42 Source #

d_well'45'founded_522 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → (AgdaAny → AgdaAny → T_Acc_42) → T_Σ_14 → T_Acc_42 Source #

d_accessible_526 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → T_Acc_42 → T_Acc_42 Source #

d_well'45'founded_528 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → T_Acc_42) → AgdaAny → T_Acc_42 Source #

d_wellFounded_530 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → T_Acc_42) → AgdaAny → T_Acc_42 Source #

d__'60''8314'__534 ∷ p → p → p → p → p → p → () Source #

d_accessible_538 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → T_Acc_42 → T_Acc_42 Source #

d_accessible'8242'_540 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → T_Acc_42 → AgdaAny → T__'60''8314'__374 → T_Acc_42 Source #

d_downwardsClosed_542 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Acc_42 → T__'60''8314'__374 → T_Acc_42 Source #

d_wellFounded_546 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → AgdaAny → T_Acc_42 Source #

d_'46'generalizedField'45'A'46'a_6161 ∷ T_GeneralizeTel_6167 → T_Level_18 Source #

d_'46'generalizedField'45'A_6163 ∷ T_GeneralizeTel_6167 → () Source #

d_'46'generalizedField'45'r_6165 ∷ T_GeneralizeTel_6167 → T_Level_18 Source #

d_GeneralizeTel_6167 ∷ () Source #

data T_GeneralizeTel_6167 Source #

Constructors

C_mkGeneralizeTel_6169 T_Level_18 T_Level_18

d_'46'generalizedField'45'A'46'a_10101 ∷ T_GeneralizeTel_10107 → T_Level_18 Source #

d_'46'generalizedField'45'A_10103 ∷ T_GeneralizeTel_10107 → () Source #

d_'46'generalizedField'45'r_10105 ∷ T_GeneralizeTel_10107 → T_Level_18 Source #

d_GeneralizeTel_10107 ∷ () Source #

data T_GeneralizeTel_10107 Source #

Constructors

C_mkGeneralizeTel_10109 T_Level_18 T_Level_18