Safe HaskellNone

MAlonzo.Code.Function.Definitions

Documentation

d_Congruent_20 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> () Source #

d_Injective_28 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> () Source #

d_Surjective_38 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> () Source #

d_Bijective_40 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> () Source #

d_Inverse'737'_46 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Inverse'691'_50 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #

d_Inverse'7495'_52 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () Source #