yellowsquid/correct-obs.git - [no description]

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