Interactive Theorem Proving SoSe 2026
  • Index
  • Lectures
    • Setup
    • Intro
    • Lists
    • Decidable
    • Logic
    • Finite
    • Sorting
    • Relation
    • SKI
    • SKIx
    • Partial
    • Coinduction
    • Undecidable
  • Exercises
    • Sheet 01
    • Sheet 02
    • Sheet 03
    • Sheet 04
    • Sheet 05
    • Sheet 06
    • Sheet 07
    • Sheet 08
  • Search
------------------------------------------------------------------------
-- The Agda standard library
--
-- Order-theoretic lattices
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Relation.Binary.Lattice where

------------------------------------------------------------------------
-- Re-export various components of the lattice hierarchy

open import Relation.Binary.Lattice.Definitions public
open import Relation.Binary.Lattice.Structures public
open import Relation.Binary.Lattice.Bundles public

Built with MkDocs.

Search

From here you can search these documents. Enter your search terms below.

Keyboard Shortcuts

Keys Action
? Open this help
n Next page
p Previous page
s Search