Quotients of First-Order Structures #
This file defines prestructures and quotients of first-order structures.
Main Definitions #
A prestructure is a first-order structure with a
setoid equivalence relation on it,
such that quotienting by that equivalence relation is still a structure.
Instances of this typeclass
Instances of other typeclasses for