summaryrefslogtreecommitdiff
path: root/src/Core/Declarative.idr
AgeCommit message (Expand)Author
2023-04-08Reduce code duplication.Chloe Brown
2023-04-07Prove weakening preserves typing judgements.Chloe Brown
2023-04-07Correct definition of Eta conversion.Chloe Brown
2023-04-06Move and rename ThinWf.Chloe Brown
2023-04-06Migrate Env to use Thinned.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-01State typing respects environment equality.Chloe Brown
2023-04-01Prove composition of thinnings is well-formed.Chloe Brown
2023-04-01Define well-formed thinnings.Chloe Brown
2023-04-01Make environments do weakening lazily.Chloe Brown
2023-04-01Prove typing implies a well-formed environment.Chloe Brown
2023-04-01State properties of typing and reduction.Chloe Brown
2023-04-01Define Declarative typing rules.Chloe Brown