| Safe Haskell | None |
|---|---|
| Language | GHC2024 |
Circuit.Logics.Laws
Description
Named law functions for lattice Heyting Boolean carriers.
These are the value-level oracles: run them on concrete models so claims about "Boolean", "Heyting", or "just a lattice" can go red.
Synopsis
- law_join_assoc :: JoinSemiLattice a => a -> a -> a -> Bool
- law_join_comm :: JoinSemiLattice a => a -> a -> Bool
- law_join_idem :: JoinSemiLattice a => a -> Bool
- law_meet_assoc :: MeetSemiLattice a => a -> a -> a -> Bool
- law_meet_comm :: MeetSemiLattice a => a -> a -> Bool
- law_meet_idem :: MeetSemiLattice a => a -> Bool
- law_absorption_join :: (JoinSemiLattice a, MeetSemiLattice a) => a -> a -> Bool
- law_absorption_meet :: (JoinSemiLattice a, MeetSemiLattice a) => a -> a -> Bool
- law_heyting_refl :: Heyting a => a -> Bool
- law_heyting_mp_left :: Heyting a => a -> a -> Bool
- law_heyting_mp_right :: Heyting a => a -> a -> Bool
- law_heyting_distr :: Heyting a => a -> a -> a -> Bool
- law_excluded_middle :: Complemented a => a -> Bool
- law_noncontradiction :: Complemented a => a -> Bool
- law_double_negation :: Complemented a => a -> Bool
- latticeSuite :: (JoinSemiLattice a, MeetSemiLattice a) => a -> a -> a -> Bool
- heytingSuite :: Heyting a => a -> a -> a -> Bool
- booleanSuite :: (Heyting a, Complemented a) => a -> a -> a -> Bool
Lattice
law_join_assoc :: JoinSemiLattice a => a -> a -> a -> Bool Source #
law_join_comm :: JoinSemiLattice a => a -> a -> Bool Source #
law_join_idem :: JoinSemiLattice a => a -> Bool Source #
law_meet_assoc :: MeetSemiLattice a => a -> a -> a -> Bool Source #
law_meet_comm :: MeetSemiLattice a => a -> a -> Bool Source #
law_meet_idem :: MeetSemiLattice a => a -> Bool Source #
law_absorption_join :: (JoinSemiLattice a, MeetSemiLattice a) => a -> a -> Bool Source #
law_absorption_meet :: (JoinSemiLattice a, MeetSemiLattice a) => a -> a -> Bool Source #
Heyting
law_heyting_refl :: Heyting a => a -> Bool Source #
law_heyting_mp_left :: Heyting a => a -> a -> Bool Source #
law_heyting_mp_right :: Heyting a => a -> a -> Bool Source #
law_heyting_distr :: Heyting a => a -> a -> a -> Bool Source #
Boolean
law_excluded_middle :: Complemented a => a -> Bool Source #
law_noncontradiction :: Complemented a => a -> Bool Source #
law_double_negation :: Complemented a => a -> Bool Source #
Suites
latticeSuite :: (JoinSemiLattice a, MeetSemiLattice a) => a -> a -> a -> Bool Source #
All lattice laws on a triple of samples.
heytingSuite :: Heyting a => a -> a -> a -> Bool Source #
booleanSuite :: (Heyting a, Complemented a) => a -> a -> a -> Bool Source #