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

MAlonzo.Code.Data.Product.Relation.Binary.Pointwise.NonDependent

Documentation

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

d_'215''45'reflexive_54 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 #

d_'215''45'refl_60 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 #

d_'215''45'respects'8322'_128 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 -> T_Σ_14 #