Safe Haskell	None

MAlonzo.Code.Induction.WellFounded

Documentation

d_WfRec_22 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> ()) -> AgdaAny -> () Source #

d_Acc_42 :: p1 -> p2 -> p3 -> p4 -> p5 -> () Source #

data T_Acc_42 Source #

Constructors

C_acc_52

d_WellFounded_54 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> () Source #

d_acc'45'inverse_68 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> T_Acc_42 -> AgdaAny -> AgdaAny -> T_Acc_42 Source #

d_Acc'45'resp'45''8776'_80 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (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_104 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny -> T_Acc_42 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_wfRecBuilder_104 :: (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny -> AgdaAny Source #

d_wfRec_118 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny -> T_Acc_42 -> AgdaAny Source #

du_wfRec_118 :: (AgdaAny -> ()) -> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny -> T_Acc_42 -> AgdaAny Source #

d_unfold'45'wfRec_132 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny -> T_Acc_42 -> T__'8801'__12 Source #

d_wfRecBuilder_152 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> T_Acc_42) -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_wfRecBuilder_152 :: (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_wfRec_160 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> T_Acc_42) -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny -> AgdaAny Source #

du_wfRec_160 :: (AgdaAny -> ()) -> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny -> AgdaAny Source #

d_wfRec'45'builder_162 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> T_Acc_42) -> T_Level_14 -> (AgdaAny -> ()) -> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_wfRec'45'builder_162 :: (AgdaAny -> ()) -> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_some'45'wfRec'45'irrelevant_198 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (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_220 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (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_220 :: (AgdaAny -> ()) -> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny -> AgdaAny Source #

d_wfRec'45'builder_222 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (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_222 :: (AgdaAny -> ()) -> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_wfRecBuilder_224 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (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_224 :: (AgdaAny -> ()) -> (AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_wfRecBuilder'45'wfRec_232 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (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_258 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (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_280 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Acc_42 -> T_Acc_42 Source #

d_wellFounded_288 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42 Source #

d_accessible_308 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Acc_42 -> T_Acc_42 Source #

d_wellFounded_316 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42 Source #

d_well'45'founded_322 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42 Source #

d__'60''8314'__334 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T__'60''8314'__334 Source #

Constructors

C_'91'_'93'_342 AgdaAny
C_trans_354 AgdaAny T__'60''8314'__334 T__'60''8314'__334

d_downwardsClosed_360 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T_Acc_42 -> T__'60''8314'__334 -> T_Acc_42 Source #

d_accessible_372 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> T_Acc_42 -> T_Acc_42 Source #

d_accessible'8242'_376 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> T_Acc_42 -> AgdaAny -> T__'60''8314'__334 -> T_Acc_42 Source #

d_wellFounded_394 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42 Source #

d__'60'__420 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> () Source #

data T__'60'__420 Source #

Constructors

C_left_432 AgdaAny
C_right_442 AgdaAny

d_accessible_450 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T_Acc_42 -> (AgdaAny -> AgdaAny -> T_Acc_42) -> T_Acc_42 Source #

d_accessible'8242'_458 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T_Acc_42 -> T_Acc_42 -> (AgdaAny -> AgdaAny -> T_Acc_42) -> T_Σ_14 -> T__'60'__420 -> T_Acc_42 Source #

d_wellFounded_480 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_488 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> T_Acc_42) -> (AgdaAny -> AgdaAny -> T_Acc_42) -> T_Σ_14 -> T_Acc_42 Source #

d_accessible_492 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Acc_42 -> T_Acc_42 Source #

d_well'45'founded_494 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42 Source #

d_wellFounded_496 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42 Source #

d__'60''8314'__500 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

d_accessible_504 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> T_Acc_42 -> T_Acc_42 Source #

d_accessible'8242'_506 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> T_Acc_42 -> AgdaAny -> T__'60''8314'__334 -> T_Acc_42 Source #

d_downwardsClosed_508 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T_Acc_42 -> T__'60''8314'__334 -> T_Acc_42 Source #

d_wellFounded_512 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42 Source #