summaryrefslogtreecommitdiff
path: root/src/Soat/FirstOrder/Algebra.idr
AgeCommit message (Collapse)Author
2022-12-05Move IsAlgebra relation from type to body.Greg Brown
2022-12-05refactor: rename RawAlgebraWithRelation.Greg Brown
- RawAlgebraWithRelation -> RawSetoidAlgebra - MkRawAlgebraWithRelation -> MkRawSetoidAlgebra - rawWithRelation -> rawSetoid
2022-12-05refactor: rename MakeRawAlgebra -> MkRawAlgebra.Greg Brown
2022-12-05refactor : make Signature.T irrelevant.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-25refactor: rename Homomorphism.f -> func.Greg Brown
2022-11-25refactor: rename Algebra.rel -> relation.Greg Brown
2022-11-25Make proofs relevant.Greg Brown
2022-11-22Define first-order algebras.Greg Brown