Documentation

d__'8851'__92 :: T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny #

du__'8851'__92 :: T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny #

d_IsDistributiveLattice_116 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsLattice_120 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_isLattice_340 :: T_IsDistributiveLattice_3036 -> T_IsLattice_2962 #

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

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

d_absorptive_424 :: T_IsLattice_2962 -> T_Σ_14 #

d_isEquivalence_426 :: T_IsLattice_2962 -> T_IsEquivalence_26 #

d_'8743''45'assoc_440 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'comm_442 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8743''45'cong_444 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'assoc_452 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'comm_454 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8744''45'cong_456 :: T_IsLattice_2962 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #

d_'8851''45'isSemilattice_784 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsCommutativeBand_590 #

du_'8851''45'isSemilattice_784 :: T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsCommutativeBand_590 #

d_'8851''45'semilattice_786 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_Semilattice_10 #

du_'8851''45'semilattice_786 :: T_TotalPreorder_222 -> T_MinOperator_98 -> T_Semilattice_10 #

d_'8851''45'isSemilattice_790 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsCommutativeBand_590 #

du_'8851''45'isSemilattice_790 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_IsCommutativeBand_590 #

d_'8851''45'semilattice_792 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_Semilattice_10 #

du_'8851''45'semilattice_792 :: T_TotalPreorder_222 -> T_MaxOperator_128 -> T_Semilattice_10 #

d_'8852''45''8851''45'isLattice_794 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsLattice_2962 #

du_'8852''45''8851''45'isLattice_794 :: T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsLattice_2962 #

d_'8851''45''8852''45'isLattice_796 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsLattice_2962 #

du_'8851''45''8852''45'isLattice_796 :: T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsLattice_2962 #

d_'8851''45''8852''45'isDistributiveLattice_798 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsDistributiveLattice_3036 #

du_'8851''45''8852''45'isDistributiveLattice_798 :: T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsDistributiveLattice_3036 #

d_'8852''45''8851''45'isDistributiveLattice_800 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsDistributiveLattice_3036 #

du_'8852''45''8851''45'isDistributiveLattice_800 :: T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_IsDistributiveLattice_3036 #

d_'8852''45''8851''45'lattice_802 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_Lattice_500 #

du_'8852''45''8851''45'lattice_802 :: T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_Lattice_500 #

d_'8851''45''8852''45'lattice_804 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_Lattice_500 #

du_'8851''45''8852''45'lattice_804 :: T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_Lattice_500 #

d_'8852''45''8851''45'distributiveLattice_806 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_DistributiveLattice_584 #

du_'8852''45''8851''45'distributiveLattice_806 :: T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_DistributiveLattice_584 #

d_'8851''45''8852''45'distributiveLattice_808 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_DistributiveLattice_584 #

du_'8851''45''8852''45'distributiveLattice_808 :: T_TotalPreorder_222 -> T_MinOperator_98 -> T_MaxOperator_128 -> T_DistributiveLattice_584 #