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

MAlonzo.Code.Function.Equivalence

Documentation

d_Equivalence_16 ∷ p → p → p → p → p → p → () Source #

data T_Equivalence_16 Source #

Constructors

C_Equivalence'46'constructor_433 T_Π_16 T_Π_16 

d_to_34 ∷ T_Equivalence_16 → T_Π_16 Source #

d_from_36 ∷ T_Equivalence_16 → T_Π_16 Source #

d__'8660'__42 ∷ T_Level_18 → T_Level_18 → () → () → () Source #

d_equivalence_56 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Equivalence_16 Source #

du_equivalence_56 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Equivalence_16 Source #

d_id_66 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Equivalence_16 Source #

du_id_66 ∷ T_Equivalence_16 Source #

d__'8728'__82 ∷ 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_16 → T_Equivalence_16 → T_Equivalence_16 Source #

du__'8728'__82 ∷ T_Equivalence_16 → T_Equivalence_16 → T_Equivalence_16 Source #

d_sym_100 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Equivalence_16 → T_Equivalence_16 Source #

du_sym_100 ∷ T_Equivalence_16 → T_Equivalence_16 Source #

d_from_110 ∷ T_Equivalence_16 → T_Π_16 Source #

d_to_112 ∷ T_Equivalence_16 → T_Π_16 Source #

d_setoid_118 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 Source #

du_setoid_118 ∷ T_Setoid_44 Source #

d_'8660''45'setoid_126 ∷ T_Level_18 → T_Setoid_44 Source #

du_'8660''45'setoid_126 ∷ T_Setoid_44 Source #

d_map_154 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16) → T_Equivalence_16 → T_Equivalence_16 Source #

du_map_154 ∷ (T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16) → T_Equivalence_16 → T_Equivalence_16 Source #

d_from_168 ∷ T_Equivalence_16 → T_Π_16 Source #

d_to_170 ∷ T_Equivalence_16 → T_Π_16 Source #

d_zip_208 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → (T_Π_16 → T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T_Π_16) → T_Equivalence_16 → T_Equivalence_16 → T_Equivalence_16 Source #

du_zip_208 ∷ (T_Π_16 → T_Π_16 → T_Π_16) → (T_Π_16 → T_Π_16 → T_Π_16) → T_Equivalence_16 → T_Equivalence_16 → T_Equivalence_16 Source #