plutus-metatheory-1.60.0.0: Command line tool for running plutus core programs
Safe HaskellSafe-Inferred
LanguageHaskell2010

MAlonzo.Code.Function.Construct.Composition

Documentation

d_congruent_50 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> 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 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_congruent_50 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_injective_56 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> 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 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_injective_56 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_surjective_62 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14 #

du_surjective_62 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Σ_14) -> (AgdaAny -> T_Σ_14) -> AgdaAny -> T_Σ_14 #

d_bijective_102 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 #

du_bijective_102 :: (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 #

d_inverse'737'_134 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> 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 -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_inverse'737'_134 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'691'_140 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> 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 -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

du_inverse'691'_140 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_inverse'7495'_146 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 #

du_inverse'7495'_146 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 #

d_isCongruent_174 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> T_IsCongruent_22 -> T_IsCongruent_22 #

du_isCongruent_174 :: (AgdaAny -> AgdaAny) -> T_IsCongruent_22 -> T_IsCongruent_22 -> T_IsCongruent_22 #

d_isInjection_296 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInjection_92 -> T_IsInjection_92 -> T_IsInjection_92 #

du_isInjection_296 :: (AgdaAny -> AgdaAny) -> T_IsInjection_92 -> T_IsInjection_92 -> T_IsInjection_92 #

d_isSurjection_426 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsSurjection_162 -> T_IsSurjection_162 -> T_IsSurjection_162 #

du_isSurjection_426 :: (AgdaAny -> AgdaAny) -> T_IsSurjection_162 -> T_IsSurjection_162 -> T_IsSurjection_162 #

d_isBijection_560 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_IsBijection_238 -> T_IsBijection_238 #

du_isBijection_560 :: (AgdaAny -> AgdaAny) -> T_IsBijection_238 -> T_IsBijection_238 -> T_IsBijection_238 #

d_isLeftInverse_740 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_IsLeftInverse_322 -> T_IsLeftInverse_322 #

du_isLeftInverse_740 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsLeftInverse_322 -> T_IsLeftInverse_322 -> T_IsLeftInverse_322 #

d_isRightInverse_882 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_IsRightInverse_408 -> T_IsRightInverse_408 #

du_isRightInverse_882 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsRightInverse_408 -> T_IsRightInverse_408 -> T_IsRightInverse_408 #

d_isInverse_1020 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_IsInverse_490 -> T_IsInverse_490 #

du_isInverse_1020 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_IsInverse_490 -> T_IsInverse_490 -> T_IsInverse_490 #

d_function_1204 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44 -> T_Func_714 -> T_Func_714 -> T_Func_714 #

du_function_1204 :: T_Func_714 -> T_Func_714 -> T_Func_714 #

d_injection_1326 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_776 -> T_Injection_776 -> T_Injection_776 #

du_injection_1326 :: T_Injection_776 -> T_Injection_776 -> T_Injection_776 #

d_surjection_1460 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44 -> T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846 #

du_surjection_1460 :: T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846 #

d_bijection_1606 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44 -> T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926 #

du_bijection_1606 :: T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926 #

d_equivalence_1764 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44 -> T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714 #

du_equivalence_1764 :: T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714 #

d_leftInverse_1906 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792 #

du_leftInverse_1906 :: T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792 #

d_rightInverse_2064 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44 -> T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880 #

du_rightInverse_2064 :: T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880 #

d_inverse_2210 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44 -> T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960 #

du_inverse_2210 :: T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960 #

d__'10230''45''8728'__2376 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Func_714 -> T_Func_714 -> T_Func_714 #

du__'10230''45''8728'__2376 :: T_Func_714 -> T_Func_714 -> T_Func_714 #

d__'8611''45''8728'__2378 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Injection_776 -> T_Injection_776 -> T_Injection_776 #

du__'8611''45''8728'__2378 :: T_Injection_776 -> T_Injection_776 -> T_Injection_776 #

d__'8608''45''8728'__2380 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846 #

du__'8608''45''8728'__2380 :: T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846 #

d__'10518''45''8728'__2382 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926 #

du__'10518''45''8728'__2382 :: T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926 #

d__'8660''45''8728'__2384 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714 #

du__'8660''45''8728'__2384 :: T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714 #

d__'8617''45''8728'__2386 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792 #

du__'8617''45''8728'__2386 :: T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792 #

d__'8618''45''8728'__2388 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880 #

du__'8618''45''8728'__2388 :: T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880 #

d__'8596''45''8728'__2390 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960 #

du__'8596''45''8728'__2390 :: T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960 #

d__'8728''45''10230'__2392 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Func_714 -> T_Func_714 -> T_Func_714 #

d__'8728''45''8611'__2394 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Injection_776 -> T_Injection_776 -> T_Injection_776 #

d__'8728''45''8608'__2396 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Surjection_846 -> T_Surjection_846 -> T_Surjection_846 #

d__'8728''45''10518'__2398 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Bijection_926 -> T_Bijection_926 -> T_Bijection_926 #

d__'8728''45''8660'__2400 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Equivalence_1714 -> T_Equivalence_1714 -> T_Equivalence_1714 #

d__'8728''45''8617'__2402 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_LeftInverse_1792 -> T_LeftInverse_1792 -> T_LeftInverse_1792 #

d__'8728''45''8618'__2404 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_RightInverse_1880 -> T_RightInverse_1880 -> T_RightInverse_1880 #

d__'8728''45''8596'__2406 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> T_Inverse_1960 -> T_Inverse_1960 #