plutus-metatheory-0.1.0.0: Command line tool for running plutus core programs

Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Function.Properties.RightInverse

Documentation

d__'8776'__44 ∷ T_GeneralizeTel_407 → T_Equivalence_1714 → AgdaAny → AgdaAny → () Source #

d__'8776'__68 ∷ T_GeneralizeTel_407 → T_Equivalence_1714 → AgdaAny → AgdaAny → () Source #

d_mkRightInverse_90 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Equivalence_1714 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_RightInverse_1880 Source #

du_mkRightInverse_90 ∷ T_Equivalence_1714 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_RightInverse_1880 Source #

d_RightInverse'8658'LeftInverse_164 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_RightInverse_1880 → T_LeftInverse_1792 Source #

du_RightInverse'8658'LeftInverse_164 ∷ T_RightInverse_1880 → T_LeftInverse_1792 Source #

d_LeftInverse'8658'RightInverse_240 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_LeftInverse_1792 → T_RightInverse_1880 Source #

du_LeftInverse'8658'RightInverse_240 ∷ T_LeftInverse_1792 → T_RightInverse_1880 Source #

d_RightInverse'8658'Surjection_322 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_RightInverse_1880 → T_Surjection_846 Source #

du_RightInverse'8658'Surjection_322 ∷ T_RightInverse_1880 → T_Surjection_846 Source #

d_'46'generalizedField'45'S'46'a_395 ∷ T_GeneralizeTel_407 → T_Level_18 Source #

d_'46'generalizedField'45'S'46'ℓ'8321'_397 ∷ T_GeneralizeTel_407 → T_Level_18 Source #

d_'8618''8658''8608'_398 ∷ T_Level_18 → () → T_Level_18 → () → T_RightInverse_1880 → T_Surjection_846 Source #

du_'8618''8658''8608'_398 ∷ T_RightInverse_1880 → T_Surjection_846 Source #

d_'46'generalizedField'45'S_399 ∷ T_GeneralizeTel_407 → T_Setoid_44 Source #

d_'8618''8658''8617'_400 ∷ T_Level_18 → () → T_Level_18 → () → T_RightInverse_1880 → T_LeftInverse_1792 Source #

du_'8618''8658''8617'_400 ∷ T_RightInverse_1880 → T_LeftInverse_1792 Source #

d_'46'generalizedField'45'T'46'a_401 ∷ T_GeneralizeTel_407 → T_Level_18 Source #

d_'8617''8658''8618'_402 ∷ T_Level_18 → () → T_Level_18 → () → T_LeftInverse_1792 → T_RightInverse_1880 Source #

du_'8617''8658''8618'_402 ∷ T_LeftInverse_1792 → T_RightInverse_1880 Source #

d_'46'generalizedField'45'T'46'ℓ'8321'_403 ∷ T_GeneralizeTel_407 → T_Level_18 Source #

d_'46'generalizedField'45'T_405 ∷ T_GeneralizeTel_407 → T_Setoid_44 Source #

d_GeneralizeTel_407 ∷ () Source #

data T_GeneralizeTel_407 Source #

Constructors

C_mkGeneralizeTel_409 T_Level_18 T_Level_18 T_Setoid_44 T_Level_18 T_Level_18 T_Setoid_44

d__'8776'__436 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_RightInverse_1880 → AgdaAny → AgdaAny → () Source #

d__'8776'__460 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_RightInverse_1880 → AgdaAny → AgdaAny → () Source #

d_to'45'from_486 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_RightInverse_1880 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_to'45'from_486 ∷ T_Setoid_44 → T_Setoid_44 → T_RightInverse_1880 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #