summaryrefslogtreecommitdiff
path: root/src/Core
AgeCommit message (Expand)Author
2023-04-23Construct shape views reflexively.Chloe Brown
2023-04-23Define shape views.Chloe Brown
2023-04-23Prove escape theorems.Chloe Brown
2023-04-23Remove unnecessary dependence on equality.Chloe Brown
2023-04-23Rename for clarity.Chloe Brown
2023-04-23Prove reducibility is reflexive.Chloe Brown
2023-04-23Use custom relation for even more control.Chloe Brown
2023-04-22Package a visible induction statement.Chloe Brown
2023-04-22Define logical relation.Chloe Brown
2023-04-16Define generic equality.Chloe Brown
2023-04-16Prove weakening of reduction.Chloe Brown
2023-04-16Prove weakening of type judgements.Chloe Brown
2023-04-16Define environment extensions.Chloe Brown
2023-04-16Prove weakening a thinned term is homomorphic.Chloe Brown
2023-04-16Prove more properties about thinning composition.Chloe Brown
2023-04-16Prove reduction is deterministic.Chloe Brown
2023-04-16Prove whnfs do not reduce.Chloe Brown
2023-04-16Prove subject typing.Chloe Brown
2023-04-16Prove conversion subsumes reduction.Chloe Brown
2023-04-16Define term reduction.Chloe Brown
2023-04-15Prove environments are well-formed.Chloe Brown
2023-04-15Prove typing respects environment quotient.Chloe Brown
2023-04-15Define declarative typing rules.Chloe Brown
2023-04-15Define typing environments.Chloe Brown
2023-04-15Prove substitution respects the quotient.Chloe Brown
2023-04-15Define Term substitution.Chloe Brown
2023-04-14Define weakening.Chloe Brown
2023-04-14Define Thinnings.Chloe Brown
2023-04-14Define Terms.Chloe Brown