summaryrefslogtreecommitdiff
path: root/src/Cfe/Context/Properties.agda
AgeCommit message (Collapse)Author
2021-03-27Prove soundness of judgement.soundnessChloe Brown
2021-03-23Prove substitution into guarded variable.Chloe Brown
2021-03-23Replace transfer with shift.Chloe Brown
Prove substitution in the unguarded context.
2021-03-22Prove transfer.Chloe Brown
2021-03-21Prove judgement weakening.Chloe Brown
2021-03-20Separate Context into a different module.Chloe Brown