summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2022-12-06Add smart constructor for first-order algebras.refactor/strictGreg Brown
2022-12-06Cast algebraic structure as setoid homomorphisms.Greg Brown
2022-12-06refactor: rename pwSetoid -> Product.Greg Brown
2022-12-06refactor: split product setoid into a new module.Greg Brown
2022-12-06refactor: rename Soat.Data -> Data.Greg Brown
2022-12-06Migrate to use idris-setoid library.Greg Brown
2022-12-06Introduce more equational reasoning.Greg Brown
2022-12-06Define helper functions for extend.Greg Brown
2022-12-06Define setoid reindexing.Greg Brown
2022-12-05refactor: name arguments to long constructors.Greg Brown
2022-12-05refactor : rename homomorphism combinators.Greg Brown
- idHomo -> id - compHomo -> (.)
2022-12-05refactor: remove commented code.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
- 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-29Construct first-order algebraic coproducts.Greg Brown
2022-11-29Prove Either is a setoid.Greg Brown
2022-11-29refactor: introduce equational reasoning.Greg Brown
2022-11-29Prove Pointwise forms a setoid.Greg Brown
2022-11-29Add syntax for setoid 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-29Add conversions between indexed setoids.Greg Brown
2022-11-29Move indexed setoids and functions out of Soat.Greg Brown
2022-11-29Extract setoids to a new module.Greg Brown
2022-11-25Prove the term algebras form an initial algebra.Greg Brown
2022-11-25Make implicit variables accessible for proofs.Greg Brown
2022-11-25refactor: expand flip in most places.Greg Brown
2022-11-25Provide more bundles from algebras.Greg Brown
2022-11-25Define the trivial indexed setoid.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-25Prove index property of shuffle.Greg Brown
2022-11-25Prove curry and uncurry form an isomorphism.Greg Brown
2022-11-25Define introductors for Pointwise.Greg Brown
2022-11-25refactor: add structural comments.Greg Brown
2022-11-25Define index on Pointwise.Greg Brown
2022-11-25Define wrap and unwrap.Greg Brown
2022-11-25Prove properties about map.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-25Change recursion structure of Pointwise.Greg Brown
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 21:31:35 +0000