summaryrefslogtreecommitdiff
path: root/src/Core/Reduction.idr
AgeCommit message (Collapse)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
There correspond to lemmata 2.1--2.5 in Abel et. al.
2023-04-01Define Reduction.Chloe Brown