Copyright | (C) 2019 Oleg Grenrus |
---|---|

License | BSD-3-Clause (see the file LICENSE) |

Maintainer | Oleg Grenrus <oleg.grenrus@iki.fi> |

Safe Haskell | Safe |

Language | Haskell2010 |

## Synopsis

- class BoundedLattice a => Heyting a where

# Documentation

class BoundedLattice a => Heyting a where Source #

A Heyting algebra is a bounded lattice equipped with a binary operation \(a \to b\) of implication.

*Laws*

x`==>`

x ≡`top`

x`/\`

(x`==>`

y) ≡ x`/\`

y y`/\`

(x`==>`

y) ≡ y x`==>`

(y`/\`

z) ≡ (x`==>`

y)`/\`

(x`==>`

z)

## Instances

Heyting Bool Source # | |

Heyting () Source # | |

Heyting All Source # | |

Heyting Any Source # | |

Heyting ZeroHalfOne Source # | |

Defined in Algebra.Lattice.ZeroHalfOne (==>) :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne Source # neg :: ZeroHalfOne -> ZeroHalfOne Source # (<=>) :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne Source # | |

Heyting M2 Source # | |

Heyting a => Heyting (Identity a) Source # | |

Heyting a => Heyting (Endo a) Source # | |

(Ord a, Finite a) => Heyting (Set a) Source # | |

(Eq a, Hashable a, Finite a) => Heyting (HashSet a) Source # | |

(Ord a, Bounded a) => Heyting (Ordered a) Source # | This is interesting logic, as it satisfies both de Morgan laws; but isn't Boolean: i.e. law of exluded middle doesn't hold. |

Heyting (Free a) Source # | |

Heyting a => Heyting (b -> a) Source # | |

Heyting (Proxy a) Source # | |

Heyting a => Heyting (Const a b) Source # | |

Heyting a => Heyting (Tagged b a) Source # | |