summaryrefslogtreecommitdiff
path: root/src/Core/Thinning.idr
AgeCommit message (Expand)Author
2023-04-07Prove some (non-)identity properties.Chloe Brown
2023-04-06Add shorthand for weakening by one variable.Chloe Brown
2023-04-02Prove thinning Views are unique.Chloe Brown
2023-04-01Prove composition preserves IsNotId.Chloe Brown
2023-04-01Make type of comp more precise.Chloe Brown
2023-04-01Make the thinning View uniqueness proof implicit.Chloe Brown
2023-04-01Prove properties of thinning composition.Chloe Brown
2023-03-31Define thinning composition.Chloe Brown
2023-03-31Add default names for the View types.Chloe Brown
2023-03-31Make Views on thinnings unique.Chloe Brown
2023-03-31Define Thinnings.Chloe Brown