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

MAlonzo.Code.Function.Equality

Documentation

d_Π_16 ∷ p → p → p → p → p → p → () Source #

data T_Π_16 Source #

Constructors

C_Π'46'constructor_1171 (AgdaAny → AgdaAny) (AgdaAny → AgdaAny → AgdaAny → AgdaAny) 

d__'10216''36''10217'__38 ∷ T_Π_16 → AgdaAny → AgdaAny Source #

d_cong_40 ∷ T_Π_16 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d__'10230'__50 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → () Source #

d_id_62 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Π_16 Source #

du_id_62 ∷ T_Π_16 Source #

d__'8728'__82 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Π_16 → T_Π_16 → T_Π_16 Source #

du__'8728'__82 ∷ T_Π_16 → T_Π_16 → T_Π_16 Source #

d_const_100 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → T_Π_16 Source #

du_const_100 ∷ T_Setoid_44 → AgdaAny → T_Π_16 Source #

d_setoid_116 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_IndexedSetoid_18 → T_Setoid_44 Source #

du_setoid_116 ∷ T_Setoid_44 → T_IndexedSetoid_18 → T_Setoid_44 Source #

d__'8680'__192 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Setoid_44 Source #

du__'8680'__192 ∷ T_Setoid_44 → T_Setoid_44 → T_Setoid_44 Source #

d_'8801''45'setoid_206 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → T_IndexedSetoid_18 → T_Setoid_44 Source #

du_'8801''45'setoid_206 ∷ T_IndexedSetoid_18 → T_Setoid_44 Source #

d_flip_272 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Π_16 → T_Π_16 Source #

du_flip_272 ∷ T_Setoid_44 → T_Π_16 → T_Π_16 Source #