Documentation

d_Congruent_14 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> () Source #

d_Indiscernable_20 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> () Source #

d_Definite_26 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> Integer) -> () Source #

d_Symmetric_32 :: T_Level_14 -> () -> (AgdaAny -> AgdaAny -> Integer) -> () Source #

d_Bounded_34 :: T_Level_14 -> () -> (AgdaAny -> AgdaAny -> Integer) -> () Source #

d_TranslationInvariant_36 :: T_Level_14 -> () -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> Integer) -> () Source #

d_TriangleInequality_38 :: T_Level_14 -> () -> (AgdaAny -> AgdaAny -> Integer) -> () Source #

d_MaxTriangleInequality_40 :: T_Level_14 -> () -> (AgdaAny -> AgdaAny -> Integer) -> () Source #

d_Contracting_42 :: T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> Integer) -> () Source #

d_ContractingOnOrbits_44 :: T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> Integer) -> () Source #

d_StrictlyContracting_46 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> Integer) -> () Source #

d_StrictlyContractingOnOrbits_50 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> Integer) -> () Source #