summaryrefslogtreecommitdiff
path: root/src/Core/Reduction.idr
AgeCommit message (Expand)Author
2023-04-08Prove conversion is a generic equality.HEADmasterChloe Brown
2023-04-08Prove weakening preserves reduction.Chloe Brown
2023-04-02Move Environment module.Chloe Brown
2023-04-01Prove reduction is deterministic.Chloe Brown
2023-04-01Prove Whnfs do not reduce.Chloe Brown
2023-04-01Prove reduction subject typing.Chloe Brown
2023-04-01Prove conversion subsumes reduction.Chloe Brown
2023-04-01State properties of typing and reduction.Chloe Brown
2023-04-01Define Reduction.Chloe Brown