Documentation

d_IsDistributiveLattice_230 :: p -> p -> p -> p -> p -> () #

d_isLattice_454 :: T_IsDistributiveLattice_3036 -> T_IsLattice_2962 #

d_'8743''45'distrib'45''8744'_478 :: T_IsDistributiveLattice_3036 -> T_Σ_14 #

d_'8744''45'distrib'45''8743'_496 :: T_IsDistributiveLattice_3036 -> T_Σ_14 #

d_poset_686 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_Poset_314 #

du_poset_686 :: T_DistributiveLattice_584 -> T_Poset_314 #

d_'8743''45'idem_688 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> AgdaAny -> AgdaAny #

du_'8743''45'idem_688 :: T_DistributiveLattice_584 -> AgdaAny -> AgdaAny #

d_'8743''45'isBand_690 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_IsBand_508 #

du_'8743''45'isBand_690 :: T_DistributiveLattice_584 -> T_IsBand_508 #

d_'8743''45'isMagma_692 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_IsMagma_176 #

du_'8743''45'isMagma_692 :: T_DistributiveLattice_584 -> T_IsMagma_176 #

d_'8743''45'isOrderTheoreticJoinSemilattice_694 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_IsJoinSemilattice_22 #

du_'8743''45'isOrderTheoreticJoinSemilattice_694 :: T_DistributiveLattice_584 -> T_IsJoinSemilattice_22 #

d_'8743''45'isOrderTheoreticMeetSemilattice_696 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_IsMeetSemilattice_180 #

du_'8743''45'isOrderTheoreticMeetSemilattice_696 :: T_DistributiveLattice_584 -> T_IsMeetSemilattice_180 #

d_'8743''45'isSemigroup_698 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_IsSemigroup_472 #

du_'8743''45'isSemigroup_698 :: T_DistributiveLattice_584 -> T_IsSemigroup_472 #

d_'8743''45'isSemilattice_700 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_IsCommutativeBand_590 #

du_'8743''45'isSemilattice_700 :: T_DistributiveLattice_584 -> T_IsCommutativeBand_590 #

d_'8743''45'orderTheoreticJoinSemilattice_702 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_JoinSemilattice_14 #

du_'8743''45'orderTheoreticJoinSemilattice_702 :: T_DistributiveLattice_584 -> T_JoinSemilattice_14 #

d_'8743''45'orderTheoreticMeetSemilattice_704 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_MeetSemilattice_200 #

du_'8743''45'orderTheoreticMeetSemilattice_704 :: T_DistributiveLattice_584 -> T_MeetSemilattice_200 #

d_'8743''45'semilattice_706 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_Semilattice_10 #

du_'8743''45'semilattice_706 :: T_DistributiveLattice_584 -> T_Semilattice_10 #

d_'8743''45''8744''45'isLattice_708 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_IsLattice_2962 #

du_'8743''45''8744''45'isLattice_708 :: T_DistributiveLattice_584 -> T_IsLattice_2962 #

d_'8743''45''8744''45'lattice_710 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_Lattice_500 #

du_'8743''45''8744''45'lattice_710 :: T_DistributiveLattice_584 -> T_Lattice_500 #

d_'8744''45'idem_712 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> AgdaAny -> AgdaAny #

du_'8744''45'idem_712 :: T_DistributiveLattice_584 -> AgdaAny -> AgdaAny #

d_'8744''45'isBand_714 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_IsBand_508 #

du_'8744''45'isBand_714 :: T_DistributiveLattice_584 -> T_IsBand_508 #

d_'8744''45'isMagma_716 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_IsMagma_176 #

du_'8744''45'isMagma_716 :: T_DistributiveLattice_584 -> T_IsMagma_176 #

d_'8743''45'isOrderTheoreticJoinSemilattice_718 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_IsJoinSemilattice_22 #

du_'8743''45'isOrderTheoreticJoinSemilattice_718 :: T_DistributiveLattice_584 -> T_IsJoinSemilattice_22 #

d_'8743''45'isOrderTheoreticMeetSemilattice_720 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_IsMeetSemilattice_180 #

du_'8743''45'isOrderTheoreticMeetSemilattice_720 :: T_DistributiveLattice_584 -> T_IsMeetSemilattice_180 #

d_'8744''45'isSemigroup_722 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_IsSemigroup_472 #

du_'8744''45'isSemigroup_722 :: T_DistributiveLattice_584 -> T_IsSemigroup_472 #

d_'8744''45'isSemilattice_724 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_IsCommutativeBand_590 #

du_'8744''45'isSemilattice_724 :: T_DistributiveLattice_584 -> T_IsCommutativeBand_590 #

d_'8743''45'orderTheoreticJoinSemilattice_726 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_JoinSemilattice_14 #

du_'8743''45'orderTheoreticJoinSemilattice_726 :: T_DistributiveLattice_584 -> T_JoinSemilattice_14 #

d_'8743''45'orderTheoreticMeetSemilattice_728 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_MeetSemilattice_200 #

du_'8743''45'orderTheoreticMeetSemilattice_728 :: T_DistributiveLattice_584 -> T_MeetSemilattice_200 #

d_'8744''45'semilattice_730 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_Semilattice_10 #

du_'8744''45'semilattice_730 :: T_DistributiveLattice_584 -> T_Semilattice_10 #

d_'8744''45''8743''45'isOrderTheoreticLattice_732 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_IsLattice_340 #

du_'8744''45''8743''45'isOrderTheoreticLattice_732 :: T_DistributiveLattice_584 -> T_IsLattice_340 #

d_'8744''45''8743''45'orderTheoreticLattice_734 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_Lattice_386 #

du_'8744''45''8743''45'orderTheoreticLattice_734 :: T_DistributiveLattice_584 -> T_Lattice_386 #

d_'8743''45''8744''45'isDistributiveLattice_736 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_IsDistributiveLattice_3036 #

du_'8743''45''8744''45'isDistributiveLattice_736 :: T_DistributiveLattice_584 -> T_IsDistributiveLattice_3036 #

d_'8743''45''8744''45'distributiveLattice_738 :: T_Level_18 -> T_Level_18 -> T_DistributiveLattice_584 -> T_DistributiveLattice_584 #

du_'8743''45''8744''45'distributiveLattice_738 :: T_DistributiveLattice_584 -> T_DistributiveLattice_584 #