Examples.Demos¶

Demos of the Agda Algebras Library¶

This is the Examples.Demos module of the Agda Universal Algebra Library.

Three self-contained demonstrations: Examples.Demos.GeneralOperationsAndRelations is a linked index of the general operations-and-relations vocabulary; Examples.Demos.HSP is the frozen literate artifact of the TYPES 2021 paper, a machine-checked proof of Birkhoff's variety theorem; and Examples.Demos.ContraX is a cautionary counterexample from an early formalization attempt.

{-# OPTIONS --without-K --exact-split --safe #-}

module Examples.Demos where

open import Examples.Demos.GeneralOperationsAndRelations
open import Examples.Demos.HSP
open import Examples.Demos.ContraX