summaryrefslogtreecommitdiff
path: root/src/Cfe/Judgement/Properties.agda
AgeCommit message (Collapse)Author
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-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