| 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_WellFounded_54 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_Well'45'founded_60 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → () Source #
d_acc'45'inverse_70 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → T_Acc_42 → AgdaAny → AgdaAny → T_Acc_42 Source #
d_Acc'45'resp'45''8776'_82 ∷ 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_106 ∷ 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_106 ∷ (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny Source #
d_wfRec_120 ∷ 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_120 ∷ (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → T_Acc_42 → AgdaAny Source #
d_unfold'45'wfRec_134 ∷ 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_wfRec'45'builder_142 ∷ 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_wfRec'45'builder_142 ∷ (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → T_Acc_42 → AgdaAny → AgdaAny → AgdaAny Source #
d_wfRecBuilder_156 ∷ 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_156 ∷ (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_wfRec_164 ∷ 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_164 ∷ (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny Source #
d_wfRec'45'builder_166 ∷ 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_166 ∷ (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_some'45'wfRec'45'irrelevant_202 ∷ 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_224 ∷ 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_224 ∷ (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny Source #
d_wfRec'45'builder_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 → AgdaAny → AgdaAny Source #
du_wfRec'45'builder_226 ∷ (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_wfRecBuilder_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_wfRecBuilder_228 ∷ (AgdaAny → ()) → (AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_wfRecBuilder'45'wfRec_236 ∷ 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_262 ∷ 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_accessible_284 ∷ 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_292 ∷ 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_well'45'founded_298 ∷ 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_314 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → T_Acc_42 → T_Acc_42 Source #
d_wellFounded_322 ∷ 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_328 ∷ 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'__340 ∷ p → p → p → p → p → p → () Source #
data T__'60''8314'__340 Source #
d_downwardsClosed_366 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Acc_42 → T__'60''8314'__340 → T_Acc_42 Source #
d_accessible_378 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → T_Acc_42 → T_Acc_42 Source #
d_accessible'8242'_382 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → T_Acc_42 → AgdaAny → T__'60''8314'__340 → T_Acc_42 Source #
d_wellFounded_400 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → AgdaAny → T_Acc_42 Source #
d_downwards'45'closed_406 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Acc_42 → T__'60''8314'__340 → T_Acc_42 Source #
d_well'45'founded_408 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → AgdaAny → T_Acc_42 Source #
d__'60'__430 ∷ p → p → p → p → p → p → p → p → p → p → () Source #
data T__'60'__430 Source #
Constructors
| C_left_442 AgdaAny | |
| C_right_452 AgdaAny |
d_accessible_460 ∷ 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'_468 ∷ 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'__430 → T_Acc_42 Source #
d_wellFounded_490 ∷ 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_498 ∷ 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_502 ∷ 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_504 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → T_Acc_42) → AgdaAny → T_Acc_42 Source #
d_wellFounded_506 ∷ 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'__510 ∷ p → p → p → p → p → p → () Source #
d_accessible_514 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → T_Acc_42 → T_Acc_42 Source #
d_accessible'8242'_516 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → T_Acc_42 → AgdaAny → T__'60''8314'__340 → T_Acc_42 Source #
d_downwards'45'closed_518 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Acc_42 → T__'60''8314'__340 → T_Acc_42 Source #
d_downwardsClosed_520 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Acc_42 → T__'60''8314'__340 → T_Acc_42 Source #
d_well'45'founded_524 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → AgdaAny → T_Acc_42 Source #
d_wellFounded_526 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → AgdaAny → T_Acc_42 Source #