\module Algebra.Meta


equation a_1 … a_n proves an equation a_0 = a_{n+1} using a_1, … a_n as intermediate steps. A proof of a_i = a_{i+1} can be specified as implicit arguments between them. using, usingOnly, and hiding with a single argument can be used instead of a proof to control the context. The first implicit argument can be either a universe or a subclass of either Monoid, AddMonoid, or Order.Lattice.Bounded.MeetSemilattice. In the former case, the meta will prove an equality in a type without using any additional structure on it. In the latter case, the meta will prove an equality using only structure available in the specified class.


This meta implements the congruence closure algorithm. For example, given assumptions x = x’ and y = y’, it can prove f x y = f x’ y’.


This meta solves systems of linear equations in ordered rings using Fourier–Motzkin elimination.