summaryrefslogtreecommitdiff
path: root/src/Soat/Data/Product.idr
AgeCommit message (Expand)Author
2022-12-06refactor: rename Soat.Data -> Data.Greg Brown
2022-12-06Migrate to use idris-setoid library.Greg Brown
2022-11-29Prove Pointwise forms a setoid.Greg Brown
2022-11-29Move indexed setoids and functions out of Soat.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-25Generalise bindUnique.Greg Brown
2022-11-25Change recursion structure of Pointwise.Greg Brown
2022-11-25Change recursion structure of map.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-22Add more operations for dependent product.Greg Brown
2022-11-22Define list-dependent product of indexed family.Greg Brown