summaryrefslogtreecommitdiff
path: root/src/Core/Term
AgeCommit message (Collapse)Author
2023-04-23Define shape views.Chloe Brown
2023-04-16Define generic equality.Chloe Brown
Judgemental equality is a trivial instance.
2023-04-16Prove weakening of type judgements.Chloe Brown
This is a huge commit that has many more changes. I should split this up later.
2023-04-16Prove weakening a thinned term is homomorphic.Chloe Brown
2023-04-16Prove whnfs do not reduce.Chloe Brown
2023-04-15Define declarative typing rules.Chloe Brown
2023-04-15Prove substitution respects the quotient.Chloe Brown
2023-04-15Define Term substitution.Chloe Brown