aboutsummaryrefslogtreecommitdiff
path: root/FinMerge.agda
AgeCommit message (Collapse)Author
2024-03-18Remove with-abstractionsJacques Comeaux
2024-03-09Factor out comparisonJacques Comeaux
2024-02-22Fill in omitted proofJacques Comeaux
2024-02-21Add iterative version of glueJacques Comeaux
2024-02-20Prove merge lemmasJacques Comeaux
2024-02-20Simplify merge functionJacques Comeaux
2024-02-19Add glue function for finite setsJacques Comeaux
2024-02-16Add helper function for merging finite setsJacques Comeaux