| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Utils.List
Documentation
Constructors
| C_'91''93'_10 | |
| C__'58''60'__12 T_Bwd_6 AgdaAny |
d_bwd'45'length_16 ∷ () → T_Bwd_6 → Integer Source #
d_lemma'60''62'1_90 ∷ () → T_Bwd_6 → [AgdaAny] → T__'8801'__12 Source #
d_lemma'60''62'1''_106 ∷ () → T_Bwd_6 → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_lemma'60''62'2_118 ∷ () → T_Bwd_6 → [AgdaAny] → T__'8801'__12 Source #
d_lemma'60''62'2''_134 ∷ () → T_Bwd_6 → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_lemma'45''60''62''62''45''43''43'_148 ∷ () → T_Bwd_6 → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_lemma'45'bwd'45'foldr_172 ∷ () → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Bwd_6 → T__'8801'__12 Source #
d_'60''62''60''45'cancel'691'_194 ∷ () → T_Bwd_6 → T_Bwd_6 → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'60''62''62''91''93''45'cancel'691'_232 ∷ () → T_Bwd_6 → T_Bwd_6 → T__'8801'__12 → T__'8801'__12 Source #
d_'60''62''62''45'cancel'691'_248 ∷ () → T_Bwd_6 → T_Bwd_6 → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'60''62''62''45'cancel'737'_266 ∷ () → T_Bwd_6 → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_IList_302 ∷ p → p → p → () Source #
data T_IList_302 Source #
Constructors
| C_'91''93'_308 | |
| C__'8759'__314 AgdaAny T_IList_302 |
d__'43''43'I__324 ∷ () → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_IList_302 → T_IList_302 → T_IList_302 Source #
d_lengthT_340 ∷ () → [AgdaAny] → (AgdaAny → ()) → T_IList_302 → Integer Source #
du_lengthT_340 ∷ [AgdaAny] → Integer Source #
d_iGetIdx_350 ∷ () → [AgdaAny] → (AgdaAny → ()) → T_IList_302 → [AgdaAny] Source #
du_iGetIdx_350 ∷ [AgdaAny] → [AgdaAny] Source #
d__'58''60'I__364 ∷ () → (AgdaAny → ()) → AgdaAny → [AgdaAny] → T_IList_302 → AgdaAny → T_IList_302 Source #
du__'58''60'I__364 ∷ [AgdaAny] → T_IList_302 → AgdaAny → T_IList_302 Source #
d_'8759''45'injectiveI_390 ∷ () → (AgdaAny → ()) → AgdaAny → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → T_IList_302 → T_IList_302 → T__'8801'__12 → T__'8801'__12 → T_Σ_14 Source #
d_IBwd_396 ∷ p → p → p → () Source #
data T_IBwd_396 Source #
Constructors
| C_'91''93'_402 | |
| C__'58''60'__408 T_IBwd_396 AgdaAny |
d__'60''62''62'I__418 ∷ () → (AgdaAny → ()) → T_Bwd_6 → [AgdaAny] → T_IBwd_396 → T_IList_302 → T_IList_302 Source #
d__'60''62''60'I__436 ∷ () → (AgdaAny → ()) → T_Bwd_6 → [AgdaAny] → T_IBwd_396 → T_IList_302 → T_IBwd_396 Source #
d_lemma'60''62'I1_458 ∷ () → (AgdaAny → ()) → T_Bwd_6 → [AgdaAny] → T_IBwd_396 → T_IList_302 → T__'8801'__12 Source #
d_lemma'60''62'I2_480 ∷ () → (AgdaAny → ()) → T_Bwd_6 → [AgdaAny] → T_IBwd_396 → T_IList_302 → T__'8801'__12 Source #
d_lemma'60''62'I2''_502 ∷ () → (AgdaAny → ()) → T_Bwd_6 → [AgdaAny] → T_IBwd_396 → T_IList_302 → T__'8801'__12 Source #
d_IBwd2IList''_520 ∷ () → (AgdaAny → ()) → T_Bwd_6 → [AgdaAny] → T__'8801'__12 → T_IBwd_396 → T_IList_302 Source #
d_IBwd2IList_538 ∷ () → (AgdaAny → ()) → T_Bwd_6 → [AgdaAny] → T__'8801'__12 → T_IBwd_396 → T_IList_302 Source #
d_IList2IBwd_552 ∷ () → (AgdaAny → ()) → [AgdaAny] → T_Bwd_6 → T__'8801'__12 → T_IList_302 → T_IBwd_396 Source #
du_IList2IBwd_552 ∷ [AgdaAny] → T_IList_302 → T_IBwd_396 Source #
d_IBwd'60''62'IList_574 ∷ () → (AgdaAny → ()) → T_Bwd_6 → [AgdaAny] → T__'8801'__12 → T_IBwd_396 → T_IList_302 → T__'8801'__12 → T__'8801'__12 Source #
d_split_590 ∷ () → T_Bwd_6 → [AgdaAny] → (AgdaAny → ()) → T_IList_302 → T_Σ_14 Source #
du_split_590 ∷ T_Bwd_6 → T_IList_302 → T_Σ_14 Source #
d_bsplit_630 ∷ () → T_Bwd_6 → [AgdaAny] → (AgdaAny → ()) → T_IBwd_396 → T_Σ_14 Source #
du_bsplit_630 ∷ [AgdaAny] → T_IBwd_396 → T_Σ_14 Source #
d_inj'45'IBwd2IList_676 ∷ () → (AgdaAny → ()) → T_Bwd_6 → [AgdaAny] → T_IBwd_396 → T_IBwd_396 → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d__'8803'_'60''62''62'__684 ∷ p → p → p → p → () Source #
data T__'8803'_'60''62''62'__684 Source #
Constructors
| C_start_690 | |
| C_bubble_700 T__'8803'_'60''62''62'__684 |
d_lem'45''8803''45''60''62''62'_710 ∷ () → [AgdaAny] → T_Bwd_6 → [AgdaAny] → T__'8803'_'60''62''62'__684 → T__'8801'__12 Source #
d_lem'45''8803''45''60''62''62'''_722 ∷ () → [AgdaAny] → T_Bwd_6 → [AgdaAny] → T__'8801'__12 → T__'8803'_'60''62''62'__684 Source #
d_no'45'empty'45''8803''45''60''62''62'_744 ∷ () → T_Bwd_6 → AgdaAny → [AgdaAny] → T__'8803'_'60''62''62'__684 → T_Irrelevant_20 Source #
d_unique'45''8803''45''60''62''62'_760 ∷ () → [AgdaAny] → T_Bwd_6 → [AgdaAny] → T__'8803'_'60''62''62'__684 → T__'8803'_'60''62''62'__684 → T__'8801'__12 Source #
d_lemma'45''8803''45''60''62''62''45'refl_780 ∷ () → T_Bwd_6 → [AgdaAny] → T__'8803'_'60''62''62'__684 Source #
d_IIList_802 ∷ p → p → p → p → p → () Source #
data T_IIList_802 Source #
Constructors
| C_'91''93'_810 | |
| C__'8759'__820 AgdaAny T_IIList_802 |
d_IIBwd_832 ∷ p → p → p → p → p → () Source #
data T_IIBwd_832 Source #
Constructors
| C_'91''93'_840 | |
| C__'58''60'__850 T_IIBwd_832 AgdaAny |
d__'60''62''62'II__870 ∷ () → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Bwd_6 → [AgdaAny] → T_IBwd_396 → T_IList_302 → T_IIBwd_832 → T_IIList_802 → T_IIList_802 Source #
d_IIBwd2IIList_902 ∷ () → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Bwd_6 → [AgdaAny] → T_IBwd_396 → T_IList_302 → T__'8801'__12 → T__'8801'__12 → T_IIBwd_832 → T_IIList_802 Source #
d_splitI_924 ∷ () → T_Bwd_6 → [AgdaAny] → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IBwd_396 → T_IList_302 → T_IIList_802 → T_Σ_14 Source #
du_splitI_924 ∷ T_Bwd_6 → T_IBwd_396 → T_IIList_802 → T_Σ_14 Source #
d_bsplitI_974 ∷ () → T_Bwd_6 → [AgdaAny] → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IBwd_396 → T_IList_302 → T_IIBwd_832 → T_Σ_14 Source #
du_bsplitI_974 ∷ [AgdaAny] → T_IList_302 → T_IIBwd_832 → T_Σ_14 Source #
d_proj'45'IIList_1028 ∷ () → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Bwd_6 → [AgdaAny] → T_IBwd_396 → T_IList_302 → T_IIList_802 → AgdaAny Source #
d_proj'45'IIBwd_1074 ∷ () → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Bwd_6 → [AgdaAny] → T_IBwd_396 → T_IList_302 → T_IIBwd_832 → AgdaAny Source #
du_proj'45'IIBwd_1074 ∷ [AgdaAny] → T_IList_302 → T_IIBwd_832 → AgdaAny Source #
d__'8803'I_'60''62''62'__1110 ∷ p → p → p → p → p → p → p → p → p → () Source #
data T__'8803'I_'60''62''62'__1110 Source #
Constructors
| C_start_1120 | |
| C_bubble_1136 T__'8803'I_'60''62''62'__1110 |
d_lem'45''8803'I'45''60''62''62'1_1156 ∷ () → (AgdaAny → ()) → [AgdaAny] → T_IList_302 → T_Bwd_6 → T_IBwd_396 → [AgdaAny] → T_IList_302 → T__'8803'_'60''62''62'__684 → T__'8803'I_'60''62''62'__1110 → T__'8801'__12 Source #
d_lem'45''8803'I'45''60''62''62'1''_1178 ∷ () → (AgdaAny → ()) → [AgdaAny] → T_IList_302 → T_Bwd_6 → T_IBwd_396 → [AgdaAny] → T_IList_302 → T__'8803'_'60''62''62'__684 → T__'8803'I_'60''62''62'__1110 → T__'8801'__12 Source #
d_lem'45''8803'I'45''60''62''62'2_1200 ∷ () → (AgdaAny → ()) → [AgdaAny] → T_IList_302 → T_Bwd_6 → T_IBwd_396 → [AgdaAny] → T_IList_302 → T__'8801'__12 → T__'8801'__12 → T__'8803'I_'60''62''62'__1110 Source #
du_lem'45''8803'I'45''60''62''62'2_1200 ∷ T_Bwd_6 → T_IBwd_396 → T__'8803'I_'60''62''62'__1110 Source #
d_lem'45''8803'I'45''60''62''62'2''_1224 ∷ () → (AgdaAny → ()) → [AgdaAny] → T_IList_302 → T_Bwd_6 → T_IBwd_396 → [AgdaAny] → T_IList_302 → T__'8801'__12 → T__'8801'__12 → T__'8803'I_'60''62''62'__1110 Source #
du_lem'45''8803'I'45''60''62''62'2''_1224 ∷ T_Bwd_6 → T_IBwd_396 → T__'8803'I_'60''62''62'__1110 Source #
d_done'45''8803'I'45''60''62''62'_1238 ∷ () → (AgdaAny → ()) → [AgdaAny] → T_IList_302 → T__'8803'I_'60''62''62'__1110 Source #
du_done'45''8803'I'45''60''62''62'_1238 ∷ [AgdaAny] → T_IList_302 → T__'8803'I_'60''62''62'__1110 Source #
d_lemma'60''62'I3_1252 ∷ () → (AgdaAny → ()) → T_Bwd_6 → T_IBwd_396 → T_IList_302 → T__'8801'__12 → T__'8801'__12 Source #
d_lem'45''60''62''60'I'45'subst_1272 ∷ () → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_IList_302 → T__'8801'__12 → T__'8801'__12 Source #
d_lemma'45''60''62''62'I'45''43''43'I_1290 ∷ () → (AgdaAny → ()) → T_Bwd_6 → [AgdaAny] → [AgdaAny] → T_IBwd_396 → T_IList_302 → T_IList_302 → T__'8801'__12 Source #
d_'60''62''62'I'91''93''45'cancel'691'_1314 ∷ () → (AgdaAny → ()) → T_Bwd_6 → T_IBwd_396 → T_IBwd_396 → T__'8801'__12 → T__'8801'__12 Source #
d_'60''62''62'I'45'cancel'737'_1336 ∷ () → (AgdaAny → ()) → T_Bwd_6 → [AgdaAny] → T_IBwd_396 → T_IList_302 → T_IList_302 → T__'8801'__12 → T__'8801'__12 Source #
d_equalbyPredicate'43''43'_1394 ∷ () → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T_IList_302 → T_IList_302 → (AgdaAny → T_Irrelevant_20) → (AgdaAny → T_Irrelevant_20) → T__'8801'__12 Source #
d_equalbyPredicate_1500 ∷ () → (AgdaAny → ()) → T_Bwd_6 → T_Bwd_6 → [AgdaAny] → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T_IBwd_396 → T_IBwd_396 → (AgdaAny → T_Irrelevant_20) → (AgdaAny → T_Irrelevant_20) → T__'8801'__12 Source #
d_equalbyPredicate'43''43'I_1588 ∷ () → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_IList_302 → T_IList_302 → T_IList_302 → T_IList_302 → T_IList_302 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → ()) → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 → T_IIList_802 → T_IIList_802 → (AgdaAny → T_Irrelevant_20) → (AgdaAny → T_Irrelevant_20) → T_Σ_14 Source #
du_equalbyPredicate'43''43'I_1588 ∷ [AgdaAny] → [AgdaAny] → T_IList_302 → T_IList_302 → T_IIList_802 → T_IIList_802 → T_Σ_14 Source #
d_equalbyPredicateI_1810 ∷ () → (AgdaAny → ()) → T_Bwd_6 → T_Bwd_6 → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_IList_302 → T_IBwd_396 → T_IBwd_396 → T_IList_302 → T_IList_302 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → ()) → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 → T_IIBwd_832 → T_IIBwd_832 → (AgdaAny → T_Irrelevant_20) → (AgdaAny → T_Irrelevant_20) → T_Σ_14 Source #