summaryrefslogtreecommitdiff
path: root/src/Core
AgeCommit message (Collapse)Author
2023-04-07Correct definition of Eta conversion.Chloe Brown
2023-04-07Prove weakening interacts well with extension.Chloe Brown
2023-04-07Fix operator fixities and imports for Name.Chloe Brown
2023-04-07Prove many properties about substitutions.Chloe Brown
2023-04-07Prove term weakening respects identities.Chloe Brown
2023-04-07Prove properties of variable weakening.Chloe Brown
2023-04-07Prove some (non-)identity properties.Chloe Brown
2023-04-06Migrate Substitution to use Thinned.Chloe Brown
2023-04-06Move and rename ThinWf.Chloe Brown
Correct statement for weakening preservation.
2023-04-06Migrate Env to use Thinned.Chloe Brown
2023-04-06Define Thinned terms.Chloe Brown
This is to unify parts of Environment and Substition.
2023-04-06Add shorthand for weakening by one variable.Chloe Brown
2023-04-02Move Environment module.Chloe Brown
2023-04-02State that weakening preserves typing.Chloe Brown
2023-04-02Prove environment equality preserves typing.Chloe Brown
2023-04-02Prove environment indexing preserves equality.Chloe Brown
2023-04-02Prove term weakening is homomorphic.Chloe Brown
2023-04-02Prove variable weakening is homomorphic.Chloe Brown
2023-04-02Prove variable Views are unique.Chloe Brown
2023-04-02Prove thinning Views are unique.Chloe Brown
2023-04-01State typing respects environment equality.Chloe Brown
2023-04-01Define environment equality.Chloe Brown
2023-04-01Prove composition of thinnings is well-formed.Chloe Brown
2023-04-01Prove composition preserves IsNotId.Chloe Brown
2023-04-01Make type of comp more precise.Chloe Brown
This is in anticipation of a proof that composition preserves IsNotId.
2023-04-01Make the thinning View uniqueness proof implicit.Chloe Brown
Almost no users of the view use this proof. Hide the details from users.
2023-04-01Prove properties of thinning composition.Chloe Brown
2023-04-01Define well-formed thinnings.Chloe Brown
2023-04-01Make environments do weakening lazily.Chloe Brown
This is in anticipation for defining well-formed thinnings.
2023-04-01Fix record projection annotations.Chloe Brown
2023-04-01Prove reduction is deterministic.Chloe Brown
2023-04-01Prove Whnfs do not reduce.Chloe Brown
2023-04-01Prove reduction subject typing.Chloe Brown
2023-04-01Prove conversion subsumes reduction.Chloe Brown
2023-04-01Prove typing implies a well-formed environment.Chloe Brown
2023-04-01State properties of typing and reduction.Chloe Brown
There correspond to lemmata 2.1--2.5 in Abel et. al.
2023-04-01Define Neutrals and Whnfs.Chloe Brown
2023-04-01Define Reduction.Chloe Brown
2023-04-01Define Declarative typing rules.Chloe Brown
2023-03-31Define Env indexing.Chloe Brown
2023-03-31Define Term substitution.Chloe Brown
2023-03-31Define Term weakening.Chloe Brown
2023-03-31Define Var weakening.Chloe Brown
2023-03-31Define thinning composition.Chloe Brown
2023-03-31Add default names for the View types.Chloe Brown
2023-03-31Define Envs.Chloe Brown
2023-03-31Define Terms.Chloe Brown
2023-03-31Define Vars.Chloe Brown
2023-03-31Make Views on thinnings unique.Chloe Brown
2023-03-31Define Thinnings.Chloe Brown
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 17:58:33 +0000