summaryrefslogtreecommitdiff
path: root/src/Cfe/Expression/Base.agda
AgeCommit message (Collapse)Author
2021-04-29Finally prove that e [ μ e / zero ] ≈ μ e.Chloe Brown
Complete proof of generator.
2021-04-05Clean up the Expression hierarchy.Chloe Brown
2021-03-29Introduce < for Languages.Chloe Brown
Move around some definitions.
2021-03-27Introduce non-terminating proof of derivation existence.Chloe Brown
2021-03-20Change judgement to use variable contexts.Chloe Brown
Add some useful context transformations.
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-05Complete proofs up to Proposition 3.2 (excluding unrolling)Chloe Brown
2021-01-23Define expression equivalence.Chloe Brown
2021-01-23Define semantics of expressions.Chloe Brown
2021-01-23Define expressionsChloe Brown