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

Age	Commit message (Expand)	Author
2023-04-08	Reduce code duplication.	Chloe Brown
2023-04-07	Prove weakening preserves typing judgements.	Chloe Brown
2023-04-07	Correct definition of Eta conversion.	Chloe Brown
2023-04-07	Prove weakening interacts well with extension.	Chloe Brown
2023-04-07	Fix operator fixities and imports for Name.	Chloe Brown
2023-04-07	Prove many properties about substitutions.	Chloe Brown
2023-04-07	Prove term weakening respects identities.	Chloe Brown
2023-04-07	Prove properties of variable weakening.	Chloe Brown
2023-04-07	Prove some (non-)identity properties.	Chloe Brown
2023-04-06	Migrate Substitution to use Thinned.	Chloe Brown
2023-04-06	Move and rename ThinWf.	Chloe Brown
2023-04-06	Migrate Env to use Thinned.	Chloe Brown
2023-04-06	Define Thinned terms.	Chloe Brown
2023-04-06	Add shorthand for weakening by one variable.	Chloe Brown
2023-04-02	Move Environment module.	Chloe Brown
2023-04-02	State that weakening preserves typing.	Chloe Brown
2023-04-02	Prove environment equality preserves typing.	Chloe Brown
2023-04-02	Prove environment indexing preserves equality.	Chloe Brown
2023-04-02	Prove term weakening is homomorphic.	Chloe Brown
2023-04-02	Prove variable weakening is homomorphic.	Chloe Brown
2023-04-02	Prove variable Views are unique.	Chloe Brown
2023-04-02	Prove thinning Views are unique.	Chloe Brown
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