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

MAlonzo.Code.Function.HalfAdjointEquivalence

Documentation

d__'8771'__12 ∷ p → p → p → p → () Source #

data T__'8771'__12 Source #

Constructors

C__'8771'_'46'constructor_923 (AgdaAny → AgdaAny) (AgdaAny → AgdaAny) 

d_to_38 ∷ T__'8771'__12 → AgdaAny → AgdaAny Source #

d_from_40 ∷ T__'8771'__12 → AgdaAny → AgdaAny Source #

d_left'45'inverse'45'of_44 ∷ T__'8771'__12 → AgdaAny → T__'8801'__12 Source #

d_right'45'inverse'45'of_48 ∷ T__'8771'__12 → AgdaAny → T__'8801'__12 Source #

d_left'45'right_52 ∷ T__'8771'__12 → AgdaAny → T__'8801'__12 Source #

d_inverse_54 ∷ T_Level_18 → T_Level_18 → () → () → T__'8771'__12 → T_Inverse_58 Source #

du_inverse_54 ∷ T__'8771'__12 → T_Inverse_58 Source #

d_injective_60 ∷ T_Level_18 → T_Level_18 → () → () → T__'8771'__12 → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_'8596''8594''8771'_80 ∷ T_Level_18 → T_Level_18 → () → () → T_Inverse_58 → T__'8771'__12 Source #

du_'8596''8594''8771'_80 ∷ T_Inverse_58 → T__'8771'__12 Source #

d_right'45'inverse'45'of_122 ∷ T_Level_18 → T_Level_18 → () → () → T_Inverse_58 → AgdaAny → T__'8801'__12 Source #

d_left'45'right_132 ∷ T_Level_18 → T_Level_18 → () → () → T_Inverse_58 → AgdaAny → T__'8801'__12 Source #

d_lemma_140 ∷ T_Level_18 → T_Level_18 → () → () → T_Inverse_58 → AgdaAny → T__'8801'__12 Source #