summaryrefslogtreecommitdiff
path: root/src/Soat
AgeCommit message (Expand)Author
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
2022-11-25Change recursion structure of map.Greg Brown
2022-11-25refactor: rename x -> vGreg Brown
2022-11-25Replace (Setoid)Environment with IFunc(tion).Greg Brown
2022-11-25Define indexed function types.Greg Brown
2022-11-25Make proofs relevant.Greg Brown
2022-11-25Remove unnecessary pattern matching.Greg Brown
2022-11-25refactor: ISetoid.rel -> relationGreg Brown
2022-11-24Define lifting of first-order signatures.Greg Brown
2022-11-24Iterate over index list for dependent map.Greg Brown
2022-11-24Prove relationship between index and tabulate.Greg Brown
2022-11-24refactor: reorder definitions.Greg Brown
2022-11-22Define second-order algebras.Greg Brown
2022-11-22Define unordered sublist relation.Greg Brown
2022-11-22Add more operations for dependent product.Greg Brown
2022-11-22Define second-order signatures.Greg 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
2022-11-22Define list-dependent product of indexed family.Greg Brown
2022-11-22Define indexed relations and equivalence records.Greg Brown
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 22:39:02 +0000