summaryrefslogtreecommitdiff
path: root/src/Cfe/Type/Properties.agda
AgeCommit message (Expand)Author
2024-01-23Prove derivations are structurally unique.HEADmasterChloe Brown
2021-04-29Finally prove that e [ μ e / zero ] ≈ μ e.Chloe Brown
2021-04-12Remove unnecessary comment.Chloe Brown
2021-04-12Cleanup Type properties.Chloe Brown
2021-03-27Begin soundness proof.Chloe Brown
2021-03-27Prove satisfaction for concatenation.lemma3.5Chloe Brown
2021-03-25Prove sequential unique decomposition.Chloe Brown
2021-03-24Prove lemma 3.5 (7).Chloe Brown
2021-03-24Prove lemma 3.5 (5).Chloe Brown
2021-03-24Make progress on lemma 3.5 (4).Chloe Brown
2021-03-16Change Language definition to respects instead of custom congruence.Chloe Brown
2021-03-05Add lemma 3.5.3.Chloe Brown
2021-03-05Prove satisfiability of τε.Chloe Brown
2021-03-05Prove satisfiability for τ⊥.Chloe Brown