summaryrefslogtreecommitdiff
path: root/src/Cfe/Expression/Properties.agda
AgeCommit message (Expand)Author
2021-03-27Begin soundness proof.Chloe Brown
2021-03-16Change Language definition to respects instead of custom congruence.Chloe Brown
2021-03-13Add weakening proofs for type judgements.Chloe Brown
2021-03-05Remove incomplete unrolling proof.Chloe Brown
2021-03-05Separate out some Language properties.Chloe Brown
2021-03-05Complete proofs up to Proposition 3.2 (excluding unrolling)Chloe Brown