summaryrefslogtreecommitdiff
path: root/src/Cfe/Judgement/Properties.agda
AgeCommit message (Expand)Author
2021-03-23Prove substitution into guarded variable.Chloe Brown
2021-03-23Replace transfer with shift.Chloe Brown
2021-03-22Prove transfer.Chloe Brown
2021-03-21Prove judgement weakening.Chloe Brown
2021-03-20Introduce variable contexts.Chloe Brown
2021-03-16Change Language definition to respects instead of custom congruence.Chloe Brown
2021-03-13Move some properties to Properties.Chloe Brown
2021-03-13Add weakening proofs for type judgements.Chloe Brown