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

Age	Commit message (Expand)	Author
2023-04-01	State typing respects environment equality.	Chloe Brown
2023-04-01	Define environment equality.	Chloe Brown
2023-04-01	Prove composition of thinnings is well-formed.	Chloe Brown
2023-04-01	Prove composition preserves IsNotId.	Chloe Brown
2023-04-01	Make type of comp more precise.	Chloe Brown
2023-04-01	Make the thinning View uniqueness proof implicit.	Chloe Brown
2023-04-01	Prove properties of thinning composition.	Chloe Brown
2023-04-01	Define well-formed thinnings.	Chloe Brown
2023-04-01	Make environments do weakening lazily.	Chloe Brown
2023-04-01	Fix record projection annotations.	Chloe Brown
2023-04-01	Prove reduction is deterministic.	Chloe Brown
2023-04-01	Prove Whnfs do not reduce.	Chloe Brown
2023-04-01	Prove reduction subject typing.	Chloe Brown
2023-04-01	Prove conversion subsumes reduction.	Chloe Brown
2023-04-01	Prove typing implies a well-formed environment.	Chloe Brown
2023-04-01	State properties of typing and reduction.	Chloe Brown
2023-04-01	Define Neutrals and Whnfs.	Chloe Brown
2023-04-01	Define Reduction.	Chloe Brown
2023-04-01	Define Declarative typing rules.	Chloe Brown
2023-03-31	Define Env indexing.	Chloe Brown
2023-03-31	Define Term substitution.	Chloe Brown
2023-03-31	Define Term weakening.	Chloe Brown
2023-03-31	Define Var weakening.	Chloe Brown
2023-03-31	Define thinning composition.	Chloe Brown
2023-03-31	Add default names for the View types.	Chloe Brown
2023-03-31	Define Envs.	Chloe Brown
2023-03-31	Define Terms.	Chloe Brown
2023-03-31	Define Vars.	Chloe Brown
2023-03-31	Make Views on thinnings unique.	Chloe Brown
2023-03-31	Define Thinnings.	Chloe Brown
2023-03-31	Define Contexts.	Chloe Brown
2023-03-31	Define Names.	Chloe Brown