summaryrefslogtreecommitdiff
path: root/src/Soat/FirstOrder
AgeCommit message (Expand)Author
2022-12-05refactor : rename homomorphism combinators.Greg Brown
2022-12-05Inline definition of IsHomomorphism.Greg Brown
2022-12-05refactor: rename Homomorphism -> (~>).Greg Brown
2022-12-05Move IsAlgebra relation from type to body.Greg Brown
2022-12-05refactor: rename RawAlgebraWithRelation.Greg Brown
2022-12-05refactor: rename MakeRawAlgebra -> MkRawAlgebra.Greg Brown
2022-12-05refactor : make Signature.T irrelevant.Greg Brown
2022-11-29Construct first-order algebraic coproducts.Greg Brown
2022-11-29refactor: introduce equational reasoning.Greg Brown
2022-11-29refactor: name arguments.Greg Brown
2022-11-29Add a bundle for raw algebra with a relation.Greg Brown
2022-11-29Move indexed setoids and functions out of Soat.Greg Brown
2022-11-25Show identity and composition are homomorphisms.Greg Brown
2022-11-25Export properties of tmRel.Greg Brown
2022-11-25Prove more properties of (~=~)Greg Brown
2022-11-25refactor: fix missing newline.Greg Brown
2022-11-25refactor: rename Homomorphism.f -> func.Greg Brown
2022-11-25refactor: rename Algebra.rel -> relation.Greg Brown
2022-11-25Generalise bindUnique.Greg Brown
2022-11-25refactor: rename bind -> bindHomo.Greg Brown
2022-11-25Generalise bindTermCong.Greg Brown
2022-11-25refactor: rename x -> vGreg Brown
2022-11-25Replace (Setoid)Environment with IFunc(tion).Greg Brown
2022-11-25Make proofs relevant.Greg Brown
2022-11-25refactor: ISetoid.rel -> relationGreg Brown
2022-11-22Define first-order terms.Greg Brown
2022-11-22Define first-order algebras.Greg Brown
2022-11-22Define first-order signatures.Greg Brown
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 09:07:04 +0000